identify LeanInk exe

Stream: lean4

[Heather Macbeth]

I'm trying to use LeanInk. I think I must be using the wrong leanInk. When I try to use leanInk on one of the tests provided, either with

% leanInk a test/playground/Simple.lean

or

% build/bin/leanInk a test/playground/Simple.lean

I get almost nothing out:

% cat test/playground/Simple.lean.leanInk
[{"contents":"def add (x y : Nat) := x + y","_type":"text"}]%

But the test script passes:

% lake script run tests
Running diff tests for leanInk
Running test ./test/bench/Basic.lean using lake...
  SUCCESS
Running test ./test/playground/playground_2.lean...
  SUCCESS
Running test ./test/playground/infoTree.lean...
  SUCCESS
Running test ./test/playground/playground_3.lean...
  SUCCESS
Running test ./test/playground/Simple.lean...
  SUCCESS
...

and after running the test script the Simple.lean.leanInk file also looks correct:

% cat test/playground/Simple.lean.leanInk
[{"contents":
  [{"typeinfo": null,
    "semanticType": "Keyword",
    "raw": "def",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": {"type": "Nat → Nat → Nat", "name": "add", "_type": "typeinfo"},
    "semanticType": "Name.Variable",
    "raw": "add",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
...

[Heather Macbeth]

Could someone help me figure out from the test script where it is finding its good leanInk, so that I can also use that one?

[Alex J. Best]

Not sure if this helps you for what you are doing or not if you are just experimenting, but I literally just set up doc-gen4 (which builds leanInk files by default) on a project and it was fairly straightforward following https://github.com/leanprover/doc-gen4:
In the lakefile.lean I added

meta if get_config? env = some "dev" then -- dev is so not everyone has to build it
require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"

then ran

lake -Kenv=dev update
lake -Kenv=dev build MyPackageName:docs

and in build/doc I have a nice copy of dec-gen4 with links to the leanInk version of all my files

[Sebastian Ullrich]

The master LeanInk supports tactic infos only. doc-gen4 and the Lean docs use a fork that adds term information.

[Heather Macbeth]

@Sebastian Ullrich, thanks for the reply. Since the tests seem to be working correctly, are you saying that somehow the tests are obtaining and running a fork of LeanInk?

[Sebastian Ullrich]

Oh I completely missed that you were running the same file twice. In that case you're just missing command line arguments enabling the extra term info: https://github.com/leanprover/LeanInk/blob/main/lakefile.lean#L26

[Sebastian Ullrich]

My comments above were also wrong: it's Alectryon we use a fork of for displaying term info, not LeanInk. I shouldn't answer question from my phone on vacation!

[Heather Macbeth]

Aha! Indeed,

% leanInk a test/playground/Simple.lean --x-enable-type-info --x-enable-docStrings --x-enable-semantic-token --prettify-output

gives exactly the same output as the expected file records. Thanks!