diff --git a/leanpkg/leanpkg/config_vars.lean.in b/leanpkg/leanpkg/config_vars.lean.in deleted file mode 100644 index 2bd0bf54cb..0000000000 --- a/leanpkg/leanpkg/config_vars.lean.in +++ /dev/null @@ -1,20 +0,0 @@ -/- -Copyright (c) 2017 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Gabriel Ebner --/ - --- This `config_vars.lean` file is automatically generated by cmake from `config_vars.lean.in`. - -namespace leanpkg - -namespace lean_version - -def major : ℕ := @LEAN_VERSION_MAJOR@ -def minor : ℕ := @LEAN_VERSION_MINOR@ -def patch : ℕ := @LEAN_VERSION_PATCH@ -def is_release : bool := @LEAN_VERSION_IS_RELEASE@ ≠ 0 - -end lean_version - -end leanpkg \ No newline at end of file diff --git a/leanpkg/leanpkg/git.lean b/leanpkg/leanpkg/git.lean index e018b2cc59..0924e6c4a0 100644 --- a/leanpkg/leanpkg/git.lean +++ b/leanpkg/leanpkg/git.lean @@ -9,7 +9,7 @@ variable [io.interface] namespace leanpkg def upstream_git_branch := -if lean_version.is_release then +if lean.is_release then "lean-" ++ lean_version_string_core else "master" diff --git a/leanpkg/leanpkg/lean_version.lean b/leanpkg/leanpkg/lean_version.lean index c1a7eddf6a..3375e36f37 100644 --- a/leanpkg/leanpkg/lean_version.lean +++ b/leanpkg/leanpkg/lean_version.lean @@ -3,25 +3,22 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Gabriel Ebner -/ -import leanpkg.config_vars - namespace leanpkg -open lean_version - def lean_version_string_core := -major.repr ++ "." ++ minor.repr ++ "." ++ patch.repr +let (major, minor, patch) := lean.version in +sformat!("{major}.{minor}.{patch}") def lean_version_string := -if is_release then +if lean.is_release then lean_version_string_core else "master" def ui_lean_version_string := -if is_release then +if lean.is_release then lean_version_string_core else "master (" ++ lean_version_string_core ++ ")" -end leanpkg \ No newline at end of file +end leanpkg diff --git a/library/init/version.lean.in b/library/init/version.lean.in index 6eb3b3fc6f..a455c99f40 100644 --- a/library/init/version.lean.in +++ b/library/init/version.lean.in @@ -6,3 +6,6 @@ def lean.version : nat × nat × nat := def lean.githash : string := "@GIT_SHA1@" + +def lean.is_release : bool := +@LEAN_VERSION_IS_RELEASE@ ≠ 0 diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index bdeca44122..894b53b73a 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -462,7 +462,6 @@ add_custom_target( WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../library" ) -configure_file("${LEAN_SOURCE_DIR}/../leanpkg/leanpkg/config_vars.lean.in" "${LEAN_SOURCE_DIR}/../leanpkg/leanpkg/config_vars.lean") add_custom_target( leanpkg ALL COMMAND "${LEAN_SOURCE_DIR}/../bin/lean" --make ${LEAN_EXTRA_MAKE_OPTS}