LeanEuclid icon indicating copy to clipboard operation
LeanEuclid copied to clipboard
Published 1 month ago • verified publisher icon loganrjmurphy

Regarding the errors after running lake build

Open FlAmmmmING opened this issue 7 months ago • 2 comments

Hello! I'm very interested in your work and have recently been trying to reproduce your experiments. However, when I run lake build, a lot of errors appear in the command line. It seems that the build fails specifically for the following files:

Smt.Term

Smt.Graph

Smt.Tactic.WHNFConfigurable

Do you happen to know how to resolve this issue?

Here is the error output from the command line (cmd):

✖ [1074/1167] Building Smt.Term trace: .> LEAN_PATH=././.lake/packages/Cli/.lake/build/lib/lean:././.lake/packages/batteries/.lake/build/lib/lean:././.lake/packages/Qq/.lake/build/lib/lean:././.lake/packages/aesop/.lake/build/lib/lean:././.lake/packages/proofwidgets/.lake/build/lib/lean:././.lake/packages/importGraph/.lake/build/lib/lean:././.lake/packages/LeanSearchClient/.lake/build/lib/lean:././.lake/packages/plausible/.lake/build/lib/lean:././.lake/packages/mathlib/.lake/build/lib/lean:././.lake/packages/smt/.lake/build/lib/lean:././.lake/packages/checkdecls/.lake/build/lib/lean:././.lake/build/lib/lean /home2/jwj/.elan/toolchains/leanprover--lean4---v4.19.0/bin/lean ././.lake/packages/smt/././Smt/Term.lean -R ././.lake/packages/smt/./. -o ././.lake/packages/smt/.lake/build/lib/lean/Smt/Term.olean -i ././.lake/packages/smt/.lake/build/lib/lean/Smt/Term.ilean -c ././.lake/packages/smt/.lake/build/ir/Smt/Term.c --plugin ././.lake/packages/smt/.lake/build/lib/lean/Smt_Data_Sexp.so --plugin ././.lake/packages/smt/.lake/build/lib/lean/Smt_Dsl_Sexp.so --json error: ././.lake/packages/smt/././Smt/Term.lean:37:0: invalid atom error: ././.lake/packages/smt/././Smt/Term.lean:37:0: invalid syntax node kind 'Smt.Term.Notation.«term_»' warning: ././.lake/packages/smt/././Smt/Term.lean:84:15: List.get!has been deprecated: Usea[i]!instead. warning: ././.lake/packages/smt/././Smt/Term.lean:85:15:List.get!has been deprecated: Usea[i]!instead. warning: ././.lake/packages/smt/././Smt/Term.lean:92:15:List.get!has been deprecated: Usea[i]!instead. warning: ././.lake/packages/smt/././Smt/Term.lean:92:15:List.get!has been deprecated: Usea[i]!instead. warning: ././.lake/packages/smt/././Smt/Term.lean:92:15:List.get!has been deprecated: Usea[i]!instead. warning: ././.lake/packages/smt/././Smt/Term.lean:92:15:List.get!has been deprecated: Usea[i]!instead. warning: ././.lake/packages/smt/././Smt/Term.lean:92:15:List.get!has been deprecated: Usea[i]!instead. warning: ././.lake/packages/smt/././Smt/Term.lean:96:15:List.get!has been deprecated: Usea[i]!instead. error: Lean exited with code 1 ✖ [13343/13443] Building Smt.Graph trace: .> LEAN_PATH=././.lake/packages/Cli/.lake/build/lib/lean:././.lake/packages/batteries/.lake/build/lib/lean:././.lake/packages/Qq/.lake/build/lib/lean:././.lake/packages/aesop/.lake/build/lib/lean:././.lake/packages/proofwidgets/.lake/build/lib/lean:././.lake/packages/importGraph/.lake/build/lib/lean:././.lake/packages/LeanSearchClient/.lake/build/lib/lean:././.lake/packages/plausible/.lake/build/lib/lean:././.lake/packages/mathlib/.lake/build/lib/lean:././.lake/packages/smt/.lake/build/lib/lean:././.lake/packages/checkdecls/.lake/build/lib/lean:././.lake/build/lib/lean /home2/jwj/.elan/toolchains/leanprover--lean4---v4.19.0/bin/lean ././.lake/packages/smt/././Smt/Graph.lean -R ././.lake/packages/smt/./. -o ././.lake/packages/smt/.lake/build/lib/lean/Smt/Graph.olean -i ././.lake/packages/smt/.lake/build/lib/lean/Smt/Graph.ilean -c ././.lake/packages/smt/.lake/build/ir/Smt/Graph.c --json error: ././.lake/packages/smt/././Smt/Graph.lean:8:0: object file '/home2/jwj/.elan/toolchains/leanprover--lean4---v4.19.0/lib/lean/Lean/Data/HashMap.olean' of module Lean.Data.HashMap does not exist error: Lean exited with code 1 ✖ [13393/13443] Building Smt.Tactic.WHNFConfigurable trace: .> LEAN_PATH=././.lake/packages/Cli/.lake/build/lib/lean:././.lake/packages/batteries/.lake/build/lib/lean:././.lake/packages/Qq/.lake/build/lib/lean:././.lake/packages/aesop/.lake/build/lib/lean:././.lake/packages/proofwidgets/.lake/build/lib/lean:././.lake/packages/importGraph/.lake/build/lib/lean:././.lake/packages/LeanSearchClient/.lake/build/lib/lean:././.lake/packages/plausible/.lake/build/lib/lean:././.lake/packages/mathlib/.lake/build/lib/lean:././.lake/packages/smt/.lake/build/lib/lean:././.lake/packages/checkdecls/.lake/build/lib/lean:././.lake/build/lib/lean /home2/jwj/.elan/toolchains/leanprover--lean4---v4.19.0/bin/lean ././.lake/packages/smt/././Smt/Tactic/WHNFConfigurable.lean -R ././.lake/packages/smt/./. -o ././.lake/packages/smt/.lake/build/lib/lean/Smt/Tactic/WHNFConfigurable.olean -i ././.lake/packages/smt/.lake/build/lib/lean/Smt/Tactic/WHNFConfigurable.ilean -c ././.lake/packages/smt/.lake/build/ir/Smt/Tactic/WHNFConfigurable.c --plugin ././.lake/packages/smt/.lake/build/lib/lean/Smt_Tactic_WHNFConfigurableRef.so --json error: ././.lake/packages/smt/././Smt/Tactic/WHNFConfigurable.lean:127:27: invalid field 'getInduct', the environment does not contain 'Lean.RecursorVal.getInduct' recVal has type RecursorVal error: ././.lake/packages/smt/././Smt/Tactic/WHNFConfigurable.lean:203:34: invalid field 'getInduct', the environment does not contain 'Lean.RecursorVal.getInduct' recVal has type RecursorVal warning: ././.lake/packages/smt/././Smt/Tactic/WHNFConfigurable.lean:226:24:Array.gethas been deprecated: Use indexing notationas[i]instead error: ././.lake/packages/smt/././Smt/Tactic/WHNFConfigurable.lean:226:36: invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor Nat warning: ././.lake/packages/smt/././Smt/Tactic/WHNFConfigurable.lean:247:19:Array.gethas been deprecated: Use indexing notationas[i]instead error: ././.lake/packages/smt/././Smt/Tactic/WHNFConfigurable.lean:247:31: invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor Nat warning: ././.lake/packages/smt/././Smt/Tactic/WHNFConfigurable.lean:276:21:Array.gethas been deprecated: Use indexing notationas[i]instead error: ././.lake/packages/smt/././Smt/Tactic/WHNFConfigurable.lean:276:33: invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor Nat warning: ././.lake/packages/smt/././Smt/Tactic/WHNFConfigurable.lean:285:21:Array.gethas been deprecated: Use indexing notationas[i]` instead error: ././.lake/packages/smt/././Smt/Tactic/WHNFConfigurable.lean:285:33: invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor Nat error: ././.lake/packages/smt/././Smt/Tactic/WHNFConfigurable.lean:343:9: invalid field 'trackZetaDelta', the environment does not contain 'Lean.Meta.Config.trackZetaDelta' cfg has type Meta.Config error: ././.lake/packages/smt/././Smt/Tactic/WHNFConfigurable.lean:344:24: expected structure error: ././.lake/packages/smt/././Smt/Tactic/WHNFConfigurable.lean:702:13: field 'config' from structure 'Lean.Meta.Context' is private error: ././.lake/packages/smt/././Smt/Tactic/WHNFConfigurable.lean:930:41: invalid field 'whnfDefault', the environment does not contain 'Lean.Meta.Cache.whnfDefault' __do_lift✝.cache has type Cache error: ././.lake/packages/smt/././Smt/Tactic/WHNFConfigurable.lean:931:41: invalid field 'whnfAll', the environment does not contain 'Lean.Meta.Cache.whnfAll' __do_lift✝.cache has type Cache error: ././.lake/packages/smt/././Smt/Tactic/WHNFConfigurable.lean:939:59: 'whnfDefault' is not a field of structure 'Cache' error: ././.lake/packages/smt/././Smt/Tactic/WHNFConfigurable.lean:940:59: 'whnfAll' is not a field of structure 'Cache' error: Lean exited with code 1 Some required builds logged failures:

  • Smt.Term
  • Smt.Graph
  • Smt.Tactic.WHNFConfigurable error: build failed

FlAmmmmING avatar May 10 '25 16:05 FlAmmmmING

Hello. May I ask if you've resolved this issue? I also tried this project today. All the steps before lake build were correct for me, but I encountered similar error messages during lake build: error: Lean exited with code 1 Some required builds logged failures:

  • Smt.Term
  • Smt.Graph
  • Smt.Tactic.WHNFConfigurable

HanksonYe avatar Jun 08 '25 09:06 HanksonYe

I reverted the commit to b50829ce4bf78e3f135b4c3421dda24514613a5a – the version from last May – and successfully configured the environment using the same method. It appears to be a compatibility issue with the newer version of mathlib.

HanksonYe avatar Jun 08 '25 15:06 HanksonYe