C API (and its tests)

Stream: general

[Utz-Uwe Haus]

I've been playing with the C-API (src/api/lean*.h) and feel that the tests may not be up to date wrt. to the current lean code base.
Should the code in src/tests/shared/ on master build and/or work?
Looking at env.c for instance it has "import standard open nat definition double (a : nat) := a + a check double 4 eval double 4" -- but that is missing # signs in front of check and eval for current syntax, and I can't find a standard module to import ...

[Kevin Buzzard]

The last commit in src/tests/shared was in 2017 and was "remove standard.lean (unused, and confusing given stdlib)".

[Kevin Buzzard]

This old blog post https://homotopytypetheory.org/2015/12/02/the-proof-assistant-lean/ seems to indicate that in Lean 1 or 2, #check was indeed check. So it seems like you're looking at super-old code which has not been brought up to date with Lean 3.

[Utz-Uwe Haus]

That is what I guessed.
Still, reading the C api headers it seems that

  lean_exception ex = 0;
  lean_env env;
  lean_options o;
  lean_ios ios;

  check(lean_options_mk_empty(&o, &ex));
  check(lean_ios_mk_std(o, &ios, &ex));
  check(lean_env_mk_std(LEAN_TRUST_HIGH, &env, &ex));
  lean_env new_env;
  lean_ios new_ios;
  check(lean_parse_commands(env, ios,
                            "import init",
                            &new_env, &new_ios, &ex));

should not give me a "no log tree in scope" exception.
What am I missing?

[Patrick Massot]

My guess is you are missing Lean 4...

[Utz-Uwe Haus]

:)
Seriously, I would be happy without a 'convenient' C++ interface -- the C one seems good enough for what I have in mind for now, but it needs to work.

[Chris Hughes]

Not sure if this is helpful, but there is a Javascript interface https://github.com/leanprover/lean-client-js It's what the VScode extension uses, so presumably it works a bit better.

[Utz-Uwe Haus]

That is using the lean server socket interface, not libleanshared.dylib

[Utz-Uwe Haus]

I guess I'll dig into how the lean server is implemented -- I'm hopeful it's only a minor glitch in the implementation of the C API lean_env_mk_std function.