nix: Undefined symbols for architecture since #16

ConnorBaker commented 2 years ago

Description

Since https://github.com/leanprover/LeanInk/commit/1830775d2fb10485e8c4f0914cdc128aafe47af7 (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 https://github.com/leanprover/LeanInk/commit/1830775d2fb10485e8c4f0914cdc128aafe47af7 and on
Alectryon version: https://github.com/Kha/alectryon/commit/c3b16f650665745e1da4ddfcc048d3bd639f71d5

Suggested fix

Additional Notes

Kha commented 2 years ago

We need two separate packages now, much like in the new-style lakefile.leans: https://github.com/leanprover/lake/blob/master/lakefile.lean. See commit above.

Kha commented 2 years ago

I extracted the relevant portions of the flake from Lean4's docs which generate pages using LeanInk

Nice. Porting more documentation to LeanInk is definitely something we're considering.

ConnorBaker commented 2 years ago

Nice. Porting more documentation to LeanInk is definitely something we're considering.

As a beginner, I think the interactivity LeanInk brings is incredibly enlightening! In particular, being able to view the proof state in-browser is extremely helpful. (I can't get enough of Lean's VS Code infoview panel -- I wish Haskell / Liquid Haskell had something similar.)

Thank you for all the work you're doing to make Lean better!

leanprover / LeanInk