Description

TODO:

Detailed behaviour

Testscenarios

References

It should compare that given an input file, e.g.: a Lean code file, the expected output given the output configuration, e.g. AlectryonFragments is generated. Basically a type of snapshot testing.

Description

Copy/paste the output of Alectryon on lean code snippets produces a big mess in your VS code text editor.

Detailed behaviour

Go to https://leanprover.github.io/lean4/doc/monads/functors.lean.html and select the first lean snippet for List.map and paste it into VS code and you will get this:

#eval
["1", "2", "3"]

List.map (λ
x =>
toString
x) [
1,
2,
3] -- ["1", "2", "3"]

Description

Defining a simple notation

prefix:max "■" => Nat.succ

produces an error

Error: unknown constant 'Lean.Syntax.Preresolved.decl'

Reproducing the issue

Lean file leanink_fail.lean:

prefix:max "■" => Nat.succ

#eval ■ 1

Run leanInk analyze leanink_fail.lean, the resulting leanink_fail.lean.leanInk is:

[{"messages":[{"contents":"Error: unknown constant 'Lean.Syntax.Preresolved.decl'","_type":"message"},{"contents":"Error: unknown constant 'Lean.Syntax.Preresolved.namespace'","_type":"message"}],"goals":[],"contents":"prefix:max \"■\" => Nat.succ","_type":"sentence"},{"contents":"\n\n#eval ","_type":"text"},{"messages":[{"contents":"Error: elaboration function for '«term■_»' has not been implemented\n  ■1","_type":"message"}],"goals":[],"contents":"■ 1","_type":"sentence"},{"contents":"\n","_type":"text"}]

Environment information

Operating System: Ubuntu 20.04
LeanInk version: 037440a09fbd321ea6bdf9c8001b64ed122060e0

Description

Is there a way to hide this lean import at the top of this chapter on the State monad?

Detailed behaviour

Testscenarios

References

Description

Attempting to use leanInk with a Lean file which relies on Mathlib, and following the instructions in the README.

My file has the following imports:

import Init.Prelude
import Mathlib.Data.Nat.Basic
import Lean

If I remove these, then leanInk works without failure...

❯ leanInk a ProgrammingLanguageSemantics.lean
Starting Analysis for: "ProgrammingLanguageSemantics.lean"

But I need these, obviously.

First try, no external deps:

❯ leanInk a ProgrammingLanguageSemantics.lean
Starting Analysis for: "ProgrammingLanguageSemantics.lean"
ERROR(1): ProgrammingLanguageSemantics.lean:1:0: error: unknown package 'Mathlib'

uncaught exception: Errors during import; aborting

Second try, with external deps, using a lakefile.lean:

❯ leanInk analyze ProgrammingLanguageSemantics.lean --lake lakefile.lean
Starting Analysis for: "ProgrammingLanguageSemantics.lean"
error: unknown command 'print-paths'
uncaught exception: Using lake failed! Make sure that lake is installed!

Expected behaviour

Expected it to work, as per the README.

Environment information

• Operating System: MacOS 14.0
• Lean version: nightly-2023-08-19
• LeanInk version: 1.0.0
• Alectryon version: 1.5.0-dev

Note that I was able to reproduce on current stable, and by updating the toolchain in leanInk to run on stable.

Features necessary to make LeanInk prototype work:

• Load LeanFile
• Encode result in AlectryonFragments format (json format).
• Split LeanFile in Text and Sentence, according to the AlectryonFormat. Each Text is, as the name suggest, only a plain text fragment that gets rendered in the output file. A Sentence additionally includes messages and goals. (we should probably document the whole interface format separately).
• Record errors within the LeanFile? Crash on error or continue as good as we can?

Description

TODO:

Detailed behaviour

Testscenarios

References

Description

To execute a lean file, we need to load the local search paths to get access to Lean module, most importantly the Init module.

Detailed behaviour

We can either manually search through the system to find the Lean search paths or use a similar approach to either Lake or LeanServer.

However getting the searchPaths for Lean is only a part of the problem that needs to be solved.
Another problem resides in third party dependencies and on disk file dependencies. Because in the current solution, the Lean4 Alectryon driver generates a new local temporary Lean file and calls LeanInk on that file. However if this file contains references, e.g.: 3rd party lake dependencies, like mathlib, or another file in the same project, these dependencies won't be propagated over to LeanInk.
We have to find a good solution to support this case, so we can make sure the dependencies are available on analysis.

Testscenarios

References

Description

In the following definition, only the Nats outside the match seem to carry metadata

example : Nat → Nat
  | 0 => 0
  | n + 1 => by exact n

Expected behaviour

We should have type hover on 0/n/... and goals on by

Environment information

• Operating System: Linux
• Lean version: nightly-03-02
• LeanInk version: https://github.com/Kha/LeanInk/tree/main
• Alectryon version: https://github.com/insightmind/alectryon/tree/typeid

Additional Notes

Perhaps some unexpected order in the info tree?

[Elab.info] command @ ⟨3, 0⟩-⟨5, 23⟩ @ Lean.Elab.Command.elabDeclaration
  Nat → Nat : Type @ ⟨3, 10⟩-⟨3, 19⟩ @ Lean.Elab.Term.elabArrow
    Nat : Type @ ⟨3, 10⟩-⟨3, 13⟩ @ Lean.Elab.Term.elabIdent
      [.] `Nat : some Sort.{?_uniq.2} @ ⟨3, 10⟩-⟨3, 13⟩
      Nat : Type @ ⟨3, 10⟩-⟨3, 13⟩
    Nat : Type @ ⟨3, 16⟩-⟨3, 19⟩ @ Lean.Elab.Term.elabIdent
      [.] `Nat : some Sort.{?_uniq.3} @ ⟨3, 16⟩-⟨3, 19⟩
      Nat : Type @ ⟨3, 16⟩-⟨3, 19⟩
  fun x =>
    _example.match_1 (fun x => Nat) x (fun _ => 0) fun n =>
      n : <failed-to-infer-type> @ ⟨4, 2⟩†-⟨5, 23⟩ @ Lean.Elab.Term.elabExplicit
    fun x =>
      _example.match_1 (fun x => Nat) x (fun _ => 0) fun n =>
        n : <failed-to-infer-type> @ ⟨4, 2⟩†-⟨5, 23⟩ @ Lean.Elab.Term.elabFun
      Nat : Type @ ⟨4, 2⟩†-⟨5, 23⟩† @ Lean.Elab.Term.elabHole
      x (isBinder := true) : Nat @ ⟨4, 2⟩†-⟨5, 23⟩†
      _example.match_1 (fun x => Nat) x (fun _ => 0) fun n =>
        n : <failed-to-infer-type> @ ⟨4, 2⟩†-⟨5, 23⟩ @ Lean.Elab.Term.elabMatch
        x : Nat @ ⟨4, 2⟩†-⟨5, 23⟩†
        0 : Nat @ ⟨4, 4⟩-⟨4, 5⟩ @ Lean.Elab.Term.elabNumLit
        0 : Nat @ ⟨4, 9⟩-⟨4, 10⟩ @ Lean.Elab.Term.elabNumLit
        [.] `n : none @ ⟨5, 4⟩-⟨5, 5⟩
        n + 1 : Nat @ ⟨4, 2⟩†-⟨5, 9⟩ @ Lean.Elab.Term.BinOp.elabBinOp
          n : Nat @ ⟨5, 4⟩-⟨5, 5⟩ @ Lean.Elab.Term.elabIdent
            n : Nat @ ⟨5, 4⟩-⟨5, 5⟩
          1 : Nat @ ⟨5, 8⟩-⟨5, 9⟩ @ Lean.Elab.Term.elabNumLit
        Tactic @ ⟨5, 13⟩-⟨5, 23⟩
        (Term.byTactic "by" (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(group (Tactic.exact "exact" `n) [])])))
        before 
        n : Nat
        ⊢ Nat
        after no goals
          Tactic @ ⟨5, 16⟩-⟨5, 23⟩ @ Lean.Elab.Tactic.evalTacticSeq
          (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(group (Tactic.exact "exact" `n) [])]))
          before 
          n : Nat
          ⊢ Nat
          after no goals
            Tactic @ ⟨5, 16⟩-⟨5, 23⟩ @ Lean.Elab.Tactic.evalTacticSeq1Indented
            (Tactic.tacticSeq1Indented [(group (Tactic.exact "exact" `n) [])])
            before 
            n : Nat
            ⊢ Nat
            after no goals
              Tactic @ ⟨5, 16⟩-⟨5, 23⟩ @ Lean.Elab.Tactic.evalExact
              (Tactic.exact "exact" `n)
              before 
              n : Nat
              ⊢ Nat
              after no goals
                n : Nat @ ⟨5, 22⟩-⟨5, 23⟩ @ Lean.Elab.Term.elabIdent
                  n : Nat @ ⟨5, 22⟩-⟨5, 23⟩
  _example (isBinder := true) : Nat → Nat @ ⟨3, 0⟩-⟨3, 7⟩

Task

Take a look at the specifications and documentation of alectryon and figure out its extensibility.

Important points:

• How well does alectryon allow us to use the json format provided by it.
• In which degree do we need to extend its functionality to support Lean4
• Can call it directly from LeanInk, if so which way do we want to recommend?
• Find out important interface points between alectryon and a possible LeanInk interface

Description

This issues shortly describes a proposal for the CLI of LeanInk.

Detailed behaviour

Following commands should be implementation:

Commands

Generate

leanInk generate <INPUT_FILES> This command generates the respective files for the input files.
The user may supply a list of input files that can either be analyzed concurrently or sequentially. Concurrency is probably preferred here, although it's ok if the prototype only supports sequently analysis at first.

Analyze

leanInk analyze <LEAN_4_SNIPPET_FILES> similar to the generate command, this command allows the user to supply a list of input files. For each input file it will analyze the code and return the result of the analysis either using the json format of Alectryon or a proprietary solution.

Help

leanInk help and leanInk help <COMMAND>
The help command displays helpful information for LeanInk in general or a specific command.

Licenses

leanInk licenses
The licenses command displays LeanInks license as well as licenses by other tools used by LeanInk, prominently Alectryon.

Arguments

Debug

-d or --debug
Every command should support the arguments for debug output of both LeanInk as well as Alectryon when summoned.

Version

-v or --version
This command is already implemented in a basic manor. This argument may also support printing the explicit Lean4 version it supports. The last point is especially relevant because lean4 is still in active development.

Testscenarios

For testing the CLI of LeanInk we should probably provide short test scripts and evaluation files, with simple diffing between expected and actual output. We can then use this information for the CI/CD.

References

Description

Since 1830775 (part of #16), trying to use LeanInk with Nix has thrown errors similar to the following:

...
Lean-lib> ar: warning: InteractiveGoal.o truncated to InteractiveGoal
leanshared> ld: warning: directory not found for option '-L/nix/store/86kayx8xkw91i7l31zr81wdn5k0w6fdn-lean-bin-tools/lib/lean'
leanc> ld: warning: directory not found for option '-L/nix/store/86kayx8xkw91i7l31zr81wdn5k0w6fdn-lean-bin-tools/lib/lean'
lean> ld: warning: directory not found for option '-L/nix/store/bc33qgb4l6qkb6146pdjp0c624yxn5lg-leanc/lib/lean'
lean-stage1> /nix/store/86kayx8xkw91i7l31zr81wdn5k0w6fdn-lean-bin-tools/bin:
lean-stage1> leanc: File exists
LeanInk.CLI.Result> LeanInk/CLI/Result.lean:11:21: warning: unused variable `result`
LeanInk.CLI.Help> LeanInk/CLI/Help.lean:11:6: warning: unused variable `maxKeyLength`
LeanInk.CLI.Basic> LeanInk/CLI/Basic.lean:91:29: warning: unused variable `unresolvedArgs`
LeanInk.CLI.Basic> LeanInk/CLI/Basic.lean:88:19: warning: unused variable `error`
LeanInk.CLI.Basic> LeanInk/CLI/Basic.lean:99:19: warning: unused variable `error`
LeanInk.Logger> LeanInk/Logger.lean:33:34: warning: unused variable `isDebug`
LeanInk.Logger> LeanInk/Logger.lean:37:37: warning: unused variable `isDebug`
LeanInk.Analysis.SemanticToken> LeanInk/Analysis/SemanticToken.lean:34:13: warning: unused variable `range`
LeanInk.Analysis.SemanticToken> LeanInk/Analysis/SemanticToken.lean:49:24: warning: unused variable `headPos`
LeanInk.Analysis.SemanticToken> LeanInk/Analysis/SemanticToken.lean:50:23: warning: unused variable `info`
LeanInk.Analysis.SemanticToken> LeanInk/Analysis/SemanticToken.lean:49:32: warning: unused variable `tailPos`
LeanInk.Analysis.LeanContext> LeanInk/Analysis/LeanContext.lean:74:8: warning: unused variable `stdout`
LeanInk.Analysis.InfoTreeTraversal> LeanInk/Analysis/InfoTreeTraversal.lean:150:16: warning: unused variable `typeFmt`
LeanInk.Analysis.InfoTreeTraversal> LeanInk/Analysis/InfoTreeTraversal.lean:287:31: warning: unused variable `contextInfo`
LeanInk.Annotation.Alectryon> LeanInk/Annotation/Alectryon.lean:127:6: warning: unused variable `default`
LeanInk.Annotation.Alectryon> LeanInk/Annotation/Alectryon.lean:153:85: warning: unused variable `l`
LeanInk-lib> ar: warning: InfoTreeTraversal.o truncated to InfoTreeTravers
leanInk> ld: warning: directory not found for option '-L/nix/store/bc33qgb4l6qkb6146pdjp0c624yxn5lg-leanc/lib/lean'
leanInk> Undefined symbols for architecture arm64:
leanInk>   "_main", referenced from:
leanInk>      implicit entry/start for main executable
leanInk> ld: symbol(s) not found for architecture arm64
leanInk> clang-11: error: linker command failed with exit code 1 (use -v to see invocation)
error: builder for '/nix/store/626a2lrlzv0fa6b49fjqqklxx09gdzs5-leanInk.drv' failed with exit code 1;
       last 6 log lines:
       > ld: warning: directory not found for option '-L/nix/store/bc33qgb4l6qkb6146pdjp0c624yxn5lg-leanc/lib/lean'
       > Undefined symbols for architecture arm64:
       >   "_main", referenced from:
       >      implicit entry/start for main executable
       > ld: symbol(s) not found for architecture arm64
       > clang-11: error: linker command failed with exit code 1 (use -v to see invocation)
       For full logs, run 'nix log /nix/store/626a2lrlzv0fa6b49fjqqklxx09gdzs5-leanInk.drv'.
error: 1 dependencies of derivation '/nix/store/kqlfsqmk4y2wv4b3mmgnb2nvy4dxvd97-alectryon.drv' failed to build
error: 1 dependencies of derivation '/nix/store/aghm2mm0377csmym9m42gm9rymg51aja-generated-lean-markdown.drv' failed to build
error: 1 dependencies of derivation '/nix/store/8aplih3pncpyi2lf55hrpb0rfpcdpdaz-doc.drv' failed to build
error: 1 dependencies of derivation '/nix/store/w0rnswfmp7vx0y51kmvi4q1fp9ccqnyi-lean-doc.drv' failed to build

Expected behaviour

I would expect that this would work without issue, and I'm not sure immediately what's causing it (other than something that changed in that commit).

Reproducing the issue

I've reproduced this issue on both aarch64-darwin and x86_64-linux.

I extracted the relevant portions of the flake from Lean4's docs which generate pages using LeanInk and bundled it all up so I could do the same as I work through Theorem Proving in Lean 4. You can find it here: https://github.com/ConnorBaker/theorem-proving-in-lean4.

The flake uses the last-working commit for LeanInk I could find. If you remove the commit or try a newer one, you should be able to reproduce it the error I'm seeing (hopefully).

Environment information

• Operating System: macOS / WSL
• Lean version: Lean4 nightlies
• LeanInk version: Commits from 1830775 and on
• Alectryon version: Kha/alectryon@c3b16f6

Suggested fix

Additional Notes

Current behaviour

The LeanInk code snippets (like those in functors) are all nicely annotated by LeanInk, but in the process we lost support for the TryIt button that pops that snippet up in a VS code text editor so user can play with it.

Suggested behaviour

We need to include the original HTML formatted code in a hidden div somewhere with a classname the javascript can look for so it can add the TryIt button back again.

Reasoning

It's handy.

Additional notes

Current behaviour

for code that contains error we get this, and the hover tip correctly shows the error, but there is no visual clue of any error in this code:

Suggested behaviour

VS Code shows this which is nicer:

Reasoning

Additional notes

Description

If I have a bug in my book chapter, LeanInk reports these errors in the hover over tooltip, but we need a process to ensure there are no bugs in the book.

Is there a way we can run LeanInk in the CI build that will break if there are bad code snippets?

Expected behaviour

Reproducing the issue

Environment information

• Operating System:
• Lean version:
• LeanInk version:
• Alectryon version:

Suggested fix

Additional Notes

Description

This works fine in my applicative.lean source file when loaded in VS code, when when I process the book I get these weird tooltips:

Expected behaviour

Same tooltips I get in VS code, or at least not this weird error message.

Reproducing the issue

Build the reference manual with this PR: leanprover/lean4#1505

Environment information

• Operating System:
• Lean version:
• LeanInk version:
• Alectryon version:

Suggested fix

Additional Notes

Probably make repository public to use free tiers of CI/CD services.

Description

Expected behaviour

Reproducing the issue

Environment information

• Operating System:
• Lean version:
• LeanInk version:
• Alectryon version:

Suggested fix

Additional Notes

Description

Readers are saying always visible comments are more readable than the little bubbles we are adding to eval statements. So we should make this an option when generating leanink books, like the new chapter on monads.

Detailed behaviour

Even better if we can do what David is doing in his functional programming in Lean book, which is to also write the "expected" values in the book so that the tool can then verify if that is what it is seeing when evaluating the code, so it can report errors if it finds a difference. This way the book author can verify the new values, rather than blindly posting something that might be entirely an error caused by some breaking change in the Lean compiler.

Testscenarios

References

Description

Sometimes while writing you need to quote a piece of core std lib code, but you get errors already defined but you also don't want to have readable namespace hidden hacks around that code either.

So it would be nice to have what we had in mdbook with the hidden comment in the form # namespace hidden to work around this.

Detailed behaviour

Testscenarios

References

Description

LeanInk can't install itself for brew-installed elan, the error output is:

Installing LeanInk...
cp: directory /Users/[MYUSERNAME]/.elan/bin does not exist
Failed copying LeanInk to .elan/bin!

Under my .elan, ls shows:

settings.toml   tmp             toolchains      update-hashes

no sign of bin.

The elan in use is:

% ls -lhta `which elan`
[OMITTED] /usr/local/bin/elan -> ../Cellar/elan-init/1.4.1/bin/elan

Expected behaviour

LeanInk could detect if elan is intalled into ~/.elan and act accordingly such as soft-lining from /usr/local/bin/.

Reproducing the issue

# 1. Follow https://leanprover-community.github.io/install/macos.html#m1-macs--apple-silicon to install elan on M1 Macs / Apple Silicon or just `brew install elan-init` for other Macs
# 2. Install LeanInk
sh -c "$(curl https://raw.githubusercontent.com/leanprover/LeanInk/main/init.sh -sSf)"

Environment information

• Operating System: macOS Monterey 12.4 on MacBookPro (16-inch, 2021) with Apple M1 Pro
• Lean version: Lean (version 4.0.0-nightly-2022-07-10, commit 23bae264fd1f, Release)
• LeanInk version: Latest commit: 4b5e606
• Alectryon version: N/A

Suggested fix

Two options:

1. Fix the line ELAN_BIN="$HOME/.elan/bin/" in https://github.com/leanprover/LeanInk/blob/main/install.sh that assumes "that lean is already installed as expected we can assume that the .elan folder already exists and is correctly linked."
2. Fix https://github.com/Homebrew/homebrew-core/blob/HEAD/Formula/elan-init.rb to add symlink for ~/.elan as well

1 is more pratical.

Additional Notes

I've bypassed the issue by following https://github.com/leanprover/LeanInk#building-from-source and manually copy leanInk to /usr/local/bin which seems to be working fine.

This issue is an ongoing list on questions for the next meeting.

Description

In our reference manual, triple back ticked lean snippets are colored differently from LeanInk processed snippets:

Sometimes I still need a triple back ticked lean snippet because I'm copying something from lean core and I would get weird errors (which results in weird tooltips) if I tried to compile it using leanInk.

Expected behaviour

Would be nice if they were consistently colored.

Reproducing the issue

See my new Applicatives.lean chapter.

Environment information

• Operating System:
• Lean version:
• LeanInk version:
• Alectryon version:

Suggested fix

Additional Notes