Trying to use Lean Copilot to develop the std library but hitting a build dependency cycle

[tenedor]

@yangky11 @semorrison @tydeu I'd like to use Lean Copilot to develop std library proofs but the normal install instructions fail. Copilot depends on std, so std can't depend on copilot.

Should it be possible to use Lean Copilot to develop std? If so, what do you recommend?

Thanks.

---

I tried to hack this by renaming my local instance of std to be std4 but I couldn't get it working. That said, I don't know Lean's build system. If it's useful, here's what I tried:

-- lakefile.lean
-package std where
+package std4 where

-- I also added the moreLinkArgs and require LeanCopilot lines

# alias Std/ as Std4/ and create Std4.lean
ln -s Std Std4
cp Std.lean Std4.lean

# rename Std references to Std4 in both Std4.lean and all *.lean files within Std/
sed -i '' -e 's/Std/Std4/g' Std4.lean
pushd Std
for f in `find . -iname '*.lean'`; do
  sed -i '' -e 's/Std/Std4/g' $f
  sed -i '' -e 's/Std4in/Stdin/g' $f
done
popd

Running lake clean; lake build makes progress for awhile but eventually hits this:

...

[126/307] Building Std4.Lean.Meta.Simp
[127/307] Building Std4.Lean.Format
error: > LEAN_PATH=./.lake/packages/std/.lake/build/lib:./.lake/packages/aesop/.lake/build/lib:./.lake/packages/LeanCopilot/.lake/build/lib:./.lake/build/lib DYLD_LIBRARY_PATH=./.lake/build/lib /Users/atlas/.elan/toolchains/leanprover--lean4---v4.5.0-rc1/bin/lean -Dlinter.missingDocs=true ./././Std4/Tactic/CoeExt.lean -R ././. -o ./.lake/build/lib/Std4/Tactic/CoeExt.olean -i ./.lake/build/lib/Std4/Tactic/CoeExt.ilean -c ./.lake/build/ir/Std4/Tactic/CoeExt.c
error: stdout:
./././Std4/Tactic/CoeExt.lean:8:25: error: unknown namespace 'Std4'
./././Std4/Tactic/CoeExt.lean:31:10: error: unknown identifier 'elabTerm'
./././Std4/Tactic/CoeExt.lean:32:19: error: unknown identifier 'coerceToFunction?'
./././Std4/Tactic/CoeExt.lean:35:42: error: unknown identifier 'indentExpr'
./././Std4/Tactic/CoeExt.lean:39:10: error: unknown identifier 'elabTerm'
./././Std4/Tactic/CoeExt.lean:40:19: error: unknown identifier 'coerceToSort?'
./././Std4/Tactic/CoeExt.lean:43:38: error: unknown identifier 'indentExpr'
./././Std4/Tactic/CoeExt.lean:55:11: error: function expected at
  ToExpr
term has type
  ?m.2380
./././Std4/Tactic/CoeExt.lean:72:11: error: function expected at
  ToExpr
term has type
  ?m.4293
./././Std4/Tactic/CoeExt.lean:77:20: error: function expected at
  SimpleScopedEnvExtension
term has type
  ?m.4326
./././Std4/Tactic/CoeExt.lean:78:2: error: unknown identifier 'registerSimpleScopedEnvExtension'
./././Std4/Tactic/CoeExt.lean:77:20: error: function expected at
  SimpleScopedEnvExtension
term has type
  ?m.4370
./././Std4/Tactic/CoeExt.lean:76:0: error: initialization function 'Std4.Tactic.Coe.initFn._@.Std.Tactic.CoeExt._hyg.762' must have type of the form `IO <type>`
./././Std4/Tactic/CoeExt.lean:84:32: error: function expected at
  CoreM
term has type
  ?m.4428
./././Std4/Tactic/CoeExt.lean:87:5: error: unknown namespace 'PrettyPrinter.Delaborator'
./././Std4/Tactic/CoeExt.lean:94:49: error: unknown identifier 'whenPPOption'
./././Std4/Tactic/CoeExt.lean:107:57: error: function expected at
  MetaM
term has type
  ?m.4492
./././Std4/Tactic/CoeExt.lean:121:71: error: function expected at
  MetaM
term has type
  ?m.4549
./././Std4/Tactic/CoeExt.lean:137:11: error: unknown identifier 'registerBuiltinAttribute'
error: external command `/Users/atlas/.elan/toolchains/leanprover--lean4---v4.5.0-rc1/bin/lean` exited with code 1
[127/307] Building Std4.Tactic.NoMatch
[128/307] Compiling Std.Linter.UnreachableTactic
error: > LEAN_PATH=./.lake/packages/std/.lake/build/lib:./.lake/packages/aesop/.lake/build/lib:./.lake/packages/LeanCopilot/.lake/build/lib:./.lake/build/lib DYLD_LIBRARY_PATH=./.lake/build/lib /Users/atlas/.elan/toolchains/leanprover--lean4---v4.5.0-rc1/bin/lean -Dlinter.missingDocs=true ./././Std4/Lean/Format.lean -R ././. -o ./.lake/build/lib/Std4/Lean/Format.olean -i ./.lake/build/lib/Std4/Lean/Format.ilean -c ./.lake/build/ir/Std4/Lean/Format.c
error: stdout:
./././Std4/Lean/Format.lean:18:33: error: unknown identifier 'prettyM'
error: external command `/Users/atlas/.elan/toolchains/leanprover--lean4---v4.5.0-rc1/bin/lean` exited with code 1

[yangky11]

I'm not aware of a good solution.

[tenedor]

Why does Lean copilot need to be built with the Lean project it's being used on?

[yangky11]

It uses HashMap in Std and some tactics for displaying suggestions. It also uses aesop for proof search.

[tenedor]

Sorry, that wasn't my question. It makes sense for copilot to depend on Std. But usually a developer tool would get built once, and then be useable with any project. Why does copilot get built as part of the project a developer wants to use copilot on?

[tenedor]

If I had a copilot executable that I could combine with any project I was developing, I could use it to develop Std because there wouldn't be a dependency cycle.

[yangky11]

I see. That makes sense. The current status of Lean Copilot is more like a library instead of a standalone developer tool.

[tenedor]

Fair enough - it is a research project after all 😉.

Do you know if making copilot a standard dev tool would run into any issues with how lake is designed? I.e. is it just a matter of engineering on Lean copilot, or is there a deeper issue with lake?

I've been curious about warnings that a lean project needs to be at the top level of a git repository - building and version control should not be coupled! - so I'm wondering if there are dragons lurking in the build system.

[yangky11]

Regarding Lake, @tydeu is the expert.

[tydeu]

@tenedor

I've been curious about warnings that a lean project needs to be at the top level of a git repository - building and version control should not be coupled! - so I'm wondering if there are dragons lurking in the build system.

There is no hard requirement that a Lean/Lake package be at the top-level of a Git repository (or in one at all). However, certain package management features do depend on Git/GitHub. Lake uses Git to download remote dependencies and Lake makes use of GitHub for cloud releases.

[kim-em]

@tenedor, @tydeu, I think the real concern here is that we are missing lake install still, so that we can install developer tools and then use them without having to add them as a dependency to the project in which we want to use them.

@tydeu, is there an issue tracking lake install so we can point people to that as the blocker for issue like this one? I couldn't see one.

[tenedor]

@semorrison thanks that sounds like the issue. Contributors to a shared project should be able to install their own personal developer tools without infecting the shared state of the project.

@tydeu thanks for the context on Lake.

[tenedor]

@semorrison / others - do you have recommendations on how I can nonetheless try using Lean Copilot with the std library? My guess is that the best path forward is to make a new repo MyStdLib that depends on both std and lean copilot, and then use MyStdLib to develop incremental additions to std which I then port to std.

This will be limited to add-only changes, but my hunch is that's all Lean Copilot will be helpful for anyway.

[tydeu]

@semorrison

@tydeu, is there an issue tracking lake install so we can point people to that as the blocker for issue like this one? I couldn't see one.

No, not yet. I don't think anyone needed it enough yet to make an issue.

[kim-em]

🤷‍♀️ Okay, I've made the issue: leanprover/lean4#3423