max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: Lean.githash

Browse source
This commit is contained in:
Sebastian Ullrich 2021-11-02 15:25:24 +01:00 • committed by Leonardo de Moura
parent 6e45685310
commit b5e7b2ab6e
2 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Init/Meta.lean
View file

@ -22,9 +22,9 @@ def version.minor : Nat := version.getMinor ()
private constant version.getPatch (u : Unit) : Nat
def version.patch : Nat := version.getPatch ()
-- @[extern c inline "lean_mk_string(LEAN_GITHASH)"]
-- constant getGithash (u : Unit) : String
-- def githash : String := getGithash ()
@[extern "lean_get_githash"]
constant getGithash (u : Unit) : String
def githash : String := getGithash ()
@[extern c inline "LEAN_VERSION_IS_RELEASE"]
constant version.getIsRelease (u : Unit) : Bool

3
src/runtime/platform.cpp
View file

@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "runtime/object.h"
#include "githash.h"
namespace lean {
extern "C" LEAN_EXPORT obj_res lean_system_platform_nbits(obj_arg) {
@ -38,4 +39,6 @@ extern "C" LEAN_EXPORT uint8 lean_system_platform_emscripten(obj_arg) {
return 0;
#endif
}
extern "C" object * lean_get_githash() { return lean_mk_string(LEAN_GITHASH); }
}