search

hrmacbeth / math2001

Lecture notes for a course on writing proofs, on paper and in the Lean proof assistant
152 stars 59 forks source link

Unable to run locally #6

Closed arbitrary-dev closed 6 months ago

arbitrary-dev commented 7 months ago 
$ lake build
error: 'Math2001': no such file or directory (error code: 2)
  file: ./././Math2001.lean
arbitrary-dev commented 7 months ago 
$ ls -a
.    .git         html        lake-manifest.json  Library   README.md
..   .gitignore   lakefile.lean   lake-packages   Library.lean  scripts
.docker  .gitpod.yml  lakefile.olean  lean-toolchain      Math2001  .vscode
arbitrary-dev commented 7 months ago 
$ lake --version
Lake version 5.0.0-src (Lean version 4.2.0)
arbitrary-dev commented 7 months ago

Some input from the editor...

image

hrmacbeth commented 7 months ago

Thanks for the report!

To get going, it should be enough to run lake build Library; this is what's done in the Gitpod init script.

I'll look into fixing the lakefile so that lake build does that automatically, and into fixing the Std build error you report.

arbitrary-dev commented 7 months ago

To get going, it should be enough to run lake build Library

Results in even more errors 😄

log.txt

arbitrary-dev commented 7 months ago

Also this:

$ lake exe cache get
Attempting to download 3902 file(s)
Downloaded: 0 file(s) [attempted 3902/3902 = 100%] (0% success)
Warning: some files were not found in the cache.
This usually means that your local checkout of mathlib4 has diverged from upstream.
If you push your commits to a branch of the mathlib4 repository, CI will build the oleans and they will be available later.
No cache files to decompress
hrmacbeth commented 7 months ago

Strangely, I can't reproduce this. Can you please provide the full log (including the commands you typed at the command line)? We can also get more eyes on this by moving the conversation to https://leanprover.zulipchat.com/#narrow/stream/270676-lean4 if you are willing.

In the short term I do recommend the Gitpod option (details in README), since it sidesteps such issues.

arbitrary-dev commented 7 months ago

All the logs provided above have $ <command> line from which they resulted.

arbitrary-dev commented 7 months ago

Perhaps I need to download dependencies, but the manifest seems to be broken somehow...

$ lake update
warning: improperly formatted manifest: incompatible manifest version `4`
mathlib: running post-update hooks
could not execute external process 'elan'
error: mathlib: failed to fetch cache

$ head lake-manifest.json
{"version": 6,
 "packagesDir": "lake-packages",
 "packages":
 [{"git":
   {"url": "https://github.com/leanprover-community/mathlib4",
    "subDir?": null,
    "rev": "76efc30c6ac851df9dfbf6440f6371ee57bf2961",
    "opts": {},
    "name": "mathlib",
    "inputRev?": "76efc30c6ac851df9dfbf6440f6371ee57bf2961",
hrmacbeth commented 7 months ago

Ah! The issue is that you should not be running lake update. Lean projects typically come with a particular version of mathlib which they are pinned to, and are unlikely to work on other versions. Have you tried the following sequence (without lake update):

git clone https://github.com/hrmacbeth/math2001.git
cd math2001
lake exe cache get
lake build Library
arbitrary-dev commented 7 months ago 
~ $ cd ~/projects

projects $ git clone https://github.com/hrmacbeth/math2001.git
Cloning into 'math2001'...
remote: Enumerating objects: 3390, done.
remote: Counting objects: 100% (321/321), done.
remote: Compressing objects: 100% (171/171), done.
remote: Total 3390 (delta 207), reused 232 (delta 148), pack-reused 3069
Receiving objects: 100% (3390/3390), 5.10 MiB | 2.54 MiB/s, done.
Resolving deltas: 100% (2386/2386), done.

projects $ cd math2001

math2001 $ lake exe cache get
info: cloning https://github.com/leanprover-community/mathlib4 to ./lake-packages/mathlib
info: cloning https://github.com/hrmacbeth/duper to ./lake-packages/Duper
info: cloning https://github.com/robertylewis/cs22-lean-autograder to ./lake-packages/autograder
info: cloning https://github.com/leanprover/std4 to ./lake-packages/std
info: cloning https://github.com/leanprover-community/quote4 to ./lake-packages/Qq
info: cloning https://github.com/leanprover-community/aesop to ./lake-packages/aesop
info: cloning https://github.com/leanprover/lean4-cli to ./lake-packages/Cli
info: cloning https://github.com/leanprover-community/ProofWidgets4 to ./lake-packages/proofwidgets
info: [0/9] Fetching proofwidgets cloud release
info: [1/9] Building Cache.IO
info: [2/9] Compiling Cache.IO
info: [2/9] Building Cache.Hashing
info: [3/9] Compiling Cache.Hashing
info: [3/9] Building Cache.Requests
info: stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
info: [5/9] Building Cache.Main
info: [5/9] Compiling Cache.Requests
info: [6/9] Compiling Cache.Main
info: stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
info: stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
info: stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
info: [9/9] Linking cache
Attempting to download 3902 file(s)
Downloaded: 0 file(s) [attempted 3902/3902 = 100%] (0% success)
Warning: some files were not found in the cache.
This usually means that your local checkout of mathlib4 has diverged from upstream.
If you push your commits to a branch of the mathlib4 repository, CI will build the oleans and they will be available later.
No cache files to decompress

math2001 $ lake build Library
[1/21] Building Std.Lean.TagAttribute
[1/21] Building Std.Lean.Command
[1/21] Building Mathlib.Mathport.Rename
[1/22] Building Std.Tactic.Unreachable
[1/26] Building Std.Tactic.OpenPrivate
[1/27] Building Std.Util.TermUnsafe
[1/27] Building Std.Tactic.SeqFocus
[1/27] Building Std.Lean.Name
[1/32] Building Std.Lean.Position
[1/32] Building Std.Tactic.ByCases
[1/34] Building Std.Lean.Float
[1/34] Building Std.Lean.Parser
[1/34] Building Std.Lean.Tactic
[1/34] Building Std.Lean.Meta.Basic
[1/64] Building Std.Tactic.RCases
[1/200] Building Std.Lean.NameMapAttribute
[2/577] Building Std.Data.Array.Init.Basic
[3/990] Building Std.Lean.InfoTree
[4/990] Building Std.Classes.Dvd
[5/990] Building Std.Data.Ord
[6/990] Building Std.Lean.Meta.Expr
[7/990] Building Std.Lean.PersistentHashMap
[8/990] Building Std.Lean.Elab.Tactic
[9/990] Building Std.WF
[10/990] Building Std.Classes.BEq
[11/990] Building Std.Lean.Delaborator
[13/990] Building Std.Util.LibraryNote
[13/990] Building Std.Lean.Meta.LCtx
[14/990] Building Std.Util.ExtendedBinder
[15/990] Building Std.Control.ForInStep.Basic
[16/990] Building Std.Tactic.HaveI
[17/990] Building Std.Data.Fin.Init.Lemmas
[18/990] Building Std.Data.Option.Init.Lemmas
[19/990] Building Std.Data.DList
[20/990] Building Std.Data.MLList.Basic
[21/990] Building Std.Lean.CoreM
[22/990] Building Std.Data.Prod.Lex
[23/990] Compiling Std.Lean.Name
[24/990] Compiling Std.Lean.TagAttribute
[25/990] Compiling Std.Lean.Tactic
[26/990] Compiling Std.Lean.Parser
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[27/990] Compiling Std.Lean.Position
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[29/990] Compiling Std.Tactic.Unreachable
[28/990] Compiling Std.Lean.Float
[30/990] Compiling Std.Data.Ord
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[31/990] Compiling Std.Lean.InfoTree
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[32/990] Compiling Std.Data.Array.Init.Basic
[33/990] Compiling Std.Classes.Dvd
[34/990] Compiling Std.Lean.NameMapAttribute
[35/990] Compiling Std.Util.TermUnsafe
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[36/990] Compiling Std.Lean.Command
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[37/990] Compiling Std.Lean.Meta.LCtx
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[38/990] Compiling Std.Control.ForInStep.Basic
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[39/990] Compiling Std.Tactic.SeqFocus
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[40/990] Compiling Std.Tactic.ByCases
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[41/990] Linking Std.Lean.Name
[41/990] Linking Std.Lean.TagAttribute
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[42/990] Linking Std.Lean.Tactic
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[43/990] Linking Std.Lean.Parser
[43/990] Linking Std.Lean.Position
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[44/990] Linking Std.Tactic.Unreachable
[44/990] Linking Std.Data.Ord
[44/990] Linking Std.Data.Array.Init.Basic
[44/990] Building Std.Lean.Expr
[44/990] Building Std.Lean.HashMap
[44/990] Building Std.Lean.Meta.Inaccessible
[44/990] Building Std.Lean.HashSet
[45/990] Building Std.Lean.MonadBacktrack
[46/990] Building Std.Lean.PersistentHashSet
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[47/990] Building Std.Lean.Util.EnvSearch
[48/990] Building Std.Lean.Util.Path
[49/990] Building Std.Tactic.Case
[50/990] Building Std.Tactic.Exact
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[51/990] Building Std.Tactic.Instances
[52/990] Building Std.Tactic.LabelAttr
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[53/990] Building Std.Tactic.LeftRight
[54/990] Building Std.Tactic.Replace
[55/990] Building Std.Tactic.Where
[56/990] Building Mathlib.Mathport.Attributes
[57/990] Building Mathlib.Util.MemoFix
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[58/990] Building Mathlib.Init.Data.Nat.Notation
[59/990] Building Mathlib.Data.Array.Defs
[60/990] Building Mathlib.Data.KVMap
[61/990] Building Mathlib.Lean.EnvExtension
[62/990] Building Mathlib.Lean.Linter
[63/990] Building Mathlib.Tactic.SimpRw
[64/990] Building Mathlib.Lean.Elab.Term
[65/990] Building Mathlib.Lean.PrettyPrinter.Delaborator
[66/990] Building Mathlib.Util.WithWeakNamespace
[67/990] Building Mathlib.Util.Syntax
[68/990] Building Mathlib.Tactic.Coe
[69/990] Building Mathlib.Tactic.Substs
[70/990] Building Mathlib.Tactic.Spread
[71/990] Building Mathlib.Util.AssertExists
[72/990] Building Mathlib.Tactic.Classical
[73/990] Building Qq.ForLean.ReduceEval
[74/990] Building Qq.ForLean.ToExpr
[75/990] Building Qq.Typ
[76/990] Building Qq.ForLean.Do
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[77/990] Building Qq.SortLocalDecls
error: > LEAN_PATH=./lake-packages/std/build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/Cli/build/lib:./lake-packages/proofwidgets/build/lib:./lake-packages/mathlib/build/lib:./lake-packages/Duper/build/lib:./lake-packages/autograder/build/lib:./build/lib LD_LIBRARY_PATH=./lake-packages/std/build/lib /usr/bin/lean -Dlinter.missingDocs=true -DwarningAsError=true ./lake-packages/std/././Std/Tactic/Instances.lean -R ./lake-packages/std/./. -o ./lake-packages/std/build/lib/Std/Tactic/Instances.olean -i ./lake-packages/std/build/lib/Std/Tactic/Instances.ilean -c ./lake-packages/std/build/ir/Std/Tactic/Instances.c
error: stdout:
./lake-packages/std/././Std/Tactic/Instances.lean:38:47: error: unknown identifier 'tcDtConfig'
error: external command `/usr/bin/lean` exited with code 1
[77/990] Building Aesop.Check
[78/990] Building Aesop.Nanos
[79/990] Building Aesop.Options.Public
[80/990] Building Aesop.Percent
[81/990] Building Aesop.Frontend.Basic
[82/990] Building Aesop.Frontend.ElabM
[83/990] Building Mathlib.Tactic.Clear!
[84/990] Building Mathlib.Tactic.CasesM
[85/990] Building Mathlib.Tactic.NthRewrite
[86/990] Building Mathlib.Util.AtomM
[87/990] Building Mathlib.Util.SynthesizeUsing
[88/990] Building Mathlib.Lean.Exception
[89/990] Building Mathlib.Lean.Meta.Basic
[90/990] Building Mathlib.Tactic.ClearExcept
[91/990] Building Mathlib.Tactic.Clear_
[93/990] Building Mathlib.Tactic.Constructor
[93/990] Building Mathlib.Tactic.FailIfNoProgress
[94/990] Building Mathlib.Tactic.GuardGoalNums
[95/990] Building Mathlib.Tactic.GuardHypNums
[96/990] Building Mathlib.Tactic.InferParam
[97/990] Building Mathlib.Lean.SMap
[98/990] Building Mathlib.Tactic.Rename
[99/990] Building Mathlib.Tactic.Set
[100/990] Building Mathlib.Tactic.SudoSetOption
[101/990] Building Mathlib.Tactic.TypeCheck
[102/990] Building Duper.Util.Misc
[103/990] Building Duper.Expr
[104/990] Building Duper.Util.Reduction
[105/990] Building Duper.Util.MessageData
[106/990] Building Duper.Util.LazyList
[107/990] Building Duper.Util.OccursCheck
[108/990] Building Duper.Unif
[109/990] Building Duper.Match
[110/990] Linking Std.Classes.Dvd
[112/990] Linking Std.Lean.Meta.LCtx
[119/990] Compiling Std.Tactic.OpenPrivate
[119/990] Compiling Std.Lean.Meta.Basic
[122/990] Building Std.Lean.AttributeExtra
[123/990] Building Mathlib.Tactic.SimpIntro
[124/990] Linking Std.Lean.Float
[124/990] Building Std.Lean.Json
[125/990] Linking Std.Control.ForInStep.Basic
[125/990] Building Std.Data.Int.Basic
[126/990] Building Std.Data.Nat.Basic
[127/990] Building Std.Tactic.Relation.Rfl
stdout:
./lake-packages/Duper/././Duper/Unif.lean:43:18: warning: unused variable `mVarId` [linter.unusedVariables]
./lake-packages/Duper/././Duper/Unif.lean:45:18: warning: unused variable `mVarId` [linter.unusedVariables]
./lake-packages/Duper/././Duper/Unif.lean:47:32: warning: unused variable `mVarId` [linter.unusedVariables]
./lake-packages/Duper/././Duper/Unif.lean:49:33: warning: unused variable `mVarId` [linter.unusedVariables]
./lake-packages/Duper/././Duper/Unif.lean:51:18: warning: unused variable `mVarId` [linter.unusedVariables]
./lake-packages/Duper/././Duper/Unif.lean:77:40: warning: unused variable `g` [linter.unusedVariables]
./lake-packages/Duper/././Duper/Unif.lean:77:42: warning: unused variable `tt` [linter.unusedVariables]
[128/990] Linking Std.Lean.NameMapAttribute
[128/990] Building Mathlib.Tactic.Trace
[129/990] Building Mathlib.Tactic.SuccessIfFailWithMsg
[130/990] Building Mathlib.Tactic.ApplyWith
[131/990] Building Mathlib.Tactic.RunCmd
error: > LEAN_PATH=./lake-packages/std/build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/Cli/build/lib:./lake-packages/proofwidgets/build/lib:./lake-packages/mathlib/build/lib:./lake-packages/Duper/build/lib:./lake-packages/autograder/build/lib:./build/lib LD_LIBRARY_PATH=./lake-packages/std/build/lib /usr/bin/lean -Dlinter.missingDocs=true -DwarningAsError=true ./lake-packages/std/././Std/Tactic/Relation/Rfl.lean -R ./lake-packages/std/./. -o ./lake-packages/std/build/lib/Std/Tactic/Relation/Rfl.olean -i ./lake-packages/std/build/lib/Std/Tactic/Relation/Rfl.ilean -c ./lake-packages/std/build/ir/Std/Tactic/Relation/Rfl.c
error: stdout:
./lake-packages/std/././Std/Tactic/Relation/Rfl.lean:21:39: error: overloaded, errors
  failed to synthesize instance
    EmptyCollection WhnfCoreConfig

  invalid {...} notation, expected type is not of the form (C ...)
    WhnfCoreConfig
./lake-packages/std/././Std/Tactic/Relation/Rfl.lean:25:43: error: application type mismatch
  Array DiscrTree.Key
argument
  DiscrTree.Key
has type
  Bool → Type : Type 1
but is expected to have type
  Type : Type 1
./lake-packages/std/././Std/Tactic/Relation/Rfl.lean:25:43: error: application type mismatch
  Array DiscrTree.Key
argument
  DiscrTree.Key
has type
  Bool → Type : Type 1
but is expected to have type
  Type : Type 1
./lake-packages/std/././Std/Tactic/Relation/Rfl.lean:41:14: error: don't know how to synthesize implicit argument
  @DiscrTree.mkPath (?m.2912 decl x✝ kind __do_lift✝¹ __discr✝¹ fst✝¹ fst✝ targetTy rel lhs rhs __do_lift✝ y✝) rel
    reflExt.config
context:
decl : Name
x✝ : Syntax
kind : AttributeKind
declTy : Expr := ConstantInfo.type __do_lift✝¹
fst✝¹ : Array Expr
fst✝ : Array BinderInfo
targetTy : Expr
fail : MetaM PUnit :=
  Lean.throwError
    (toMessageData "@[refl] attribute only applies to lemmas proving x ∼ x, got " ++ toMessageData declTy ++
      toMessageData "")
rel lhs rhs : Expr
y✝ : PUnit
⊢ Bool
./lake-packages/std/././Std/Tactic/Relation/Rfl.lean:41:8: error: don't know how to synthesize placeholder for argument 'α'
context:
decl : Name
x✝ : Syntax
kind : AttributeKind
declTy : Expr := ConstantInfo.type __do_lift✝¹
fst✝¹ : Array Expr
fst✝ : Array BinderInfo
targetTy : Expr
fail : MetaM PUnit :=
  Lean.throwError
    (toMessageData "@[refl] attribute only applies to lemmas proving x ∼ x, got " ++ toMessageData declTy ++
      toMessageData "")
rel lhs rhs : Expr
y✝ : PUnit
⊢ Type
./lake-packages/std/././Std/Tactic/Relation/Rfl.lean:41:8: error: failed to infer binder type
./lake-packages/std/././Std/Tactic/Relation/Rfl.lean:58:2: error: failed to synthesize instance for 'for_in%' notation
  ForIn (ReaderT Meta.Context (StateRefT' IO.RealWorld Meta.State CoreM))
    (?m.5733 goal __do_lift✝³ __do_lift✝² __discr✝ rel arg✝¹ arg✝ s __do_lift✝¹) ?m.7468
./lake-packages/std/././Std/Tactic/Relation/Rfl.lean:58:2: error: invalid field notation, type is not of the form (C ...) where C is a constant
  r✝
has type
  ?m.5735 goal __do_lift✝³ __do_lift✝² __discr✝ rel arg✝¹ arg✝ s __do_lift✝¹ __do_lift✝
./lake-packages/std/././Std/Tactic/Relation/Rfl.lean:58:2: error: invalid field notation, type is not of the form (C ...) where C is a constant
  r✝
has type
  ?m.5735 goal __do_lift✝³ __do_lift✝² __discr✝ rel arg✝¹ arg✝ s __do_lift✝¹ __do_lift✝
./lake-packages/std/././Std/Tactic/Relation/Rfl.lean:68:4: error: invalid field notation, type is not of the form (C ...) where C is a constant
  sErr
has type
  ?m.7573 goal __do_lift✝³ __do_lift✝² __discr✝ rel arg✝¹ arg✝ s
./lake-packages/std/././Std/Tactic/Relation/Rfl.lean:73:0: error: invalid occurrence of universe level 'u_1' at 'Std.Tactic._aux_Std_Tactic_Relation_Rfl___elabRules_Lean_Parser_Tactic_tacticRfl_1', it does not occur at the declaration type, nor it is explicit universe level provided by the user, occurring at expression
  MVarId.applyRfl.{u_1} x✝
at declaration body
  fun (x : Syntax) =>
    let_fun __discr : Syntax := x;
    if Syntax.isOfKind __discr `Lean.Parser.Tactic.tacticRfl = true then
      let_fun __discr : Syntax := Syntax.getArg __discr 0;
      withMainContext (liftMetaFinishingTactic fun (x : MVarId) => MVarId.applyRfl x)
    else
      let_fun __discr : Syntax := x;
      throwUnsupportedSyntax
error: external command `/usr/bin/lean` exited with code 1
[131/990] Building Std.Util.Pickle
[132/990] Building Std.CodeAction.Attr
stdout:
./lake-packages/Duper/././Duper/Match.lean:69:29: warning: unused variable `match_target_hd` [linter.unusedVariables]
./lake-packages/Duper/././Duper/Match.lean:69:45: warning: unused variable `match_target_tl` [linter.unusedVariables]
[133/990] Building Std.Tactic.GuardExpr
[134/990] Building Mathlib.Tactic.ProjectionNotation
[135/990] Building Mathlib.Tactic.PPWithUniv
[136/990] Building Std.Control.ForInStep.Lemmas
[137/990] Linking Std.Lean.InfoTree
[137/990] Linking Std.Util.TermUnsafe
[138/990] Linking Std.Lean.Command
[138/990] Linking Std.Tactic.SeqFocus
[138/990] Linking Std.Tactic.ByCases
[138/990] Compiling Duper.Util.MessageData
[141/990] Building Std.Tactic.PrintDependents
[141/990] Building Std.Tactic.CoeExt
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[142/990] Compiling Std.Lean.Json
[143/990] Compiling Std.Lean.AttributeExtra
[144/990] Compiling Duper.Unif
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[146/990] Compiling Duper.Util.Reduction
[147/990] Compiling Duper.Util.OccursCheck
[148/990] Compiling Duper.Match
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[149/990] Compiling Std.Data.Nat.Basic
stdout:
./lake-packages/Duper/././Duper/Expr.lean:257:6: warning: unused variable `e` [linter.unusedVariables]
[155/990] Building Std.Data.Array.Basic
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[156/990] Building Std.Tactic.Lint.Basic
[157/990] Compiling Duper.Expr
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[158/990] Building Std.Linter.UnreachableTactic
[159/990] Compiling Std.Data.Array.Basic
[160/990] Linking Duper.Util.MessageData
[160/990] Linking Std.Lean.Json
[160/990] Linking Std.Lean.AttributeExtra
[160/990] Building Mathlib.Util.WhatsNew
[161/990] Building Std.Lean.Format
[162/990] Building Std.Tactic.NoMatch
[163/990] Building Mathlib.Tactic.ExtractGoal
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[164/990] Building Std.Tactic.PrintPrefix
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[165/990] Building Mathlib.Control.ULift
[166/990] Building Mathlib.Init.Quot
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[167/990] Building Mathlib.Init.Data.Ordering.Basic
[168/990] Building Mathlib.Data.MLList.Basic
[169/990] Building Mathlib.Tactic.UnsetOption
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[170/990] Building Mathlib.Tactic.HaveI
[171/990] Building Mathlib.Init.Data.Fin.Basic
[172/990] Building Library.Tactic.Rel.Attr
[173/990] Building Mathlib.Tactic.Monotonicity.Attr
[175/990] Building Mathlib.Tactic.Attr.Register
[175/990] Building Std.Test.Internal.DummyLabelAttr
[176/990] Building Mathlib.Tactic.Have
[177/990] Building Mathlib.Tactic.ScopedNS
[178/990] Building Std.Classes.SetNotation
[179/990] Building Std.Tactic.Relation.Symm
[180/990] Building Std.Lean.Meta.InstantiateMVars
[181/990] Building Std.Lean.Meta.Clear
[182/990] Building Std.Lean.Meta.AssertHypotheses
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[183/990] Building Aesop.Constants
[184/990] Building Mathlib.Tactic.ApplyAt
[186/990] Linking Std.Tactic.OpenPrivate
[189/990] Linking Std.Data.Nat.Basic
[190/990] Compiling Std.CodeAction.Attr
[190/990] Compiling Std.Lean.Format
[191/990] Compiling Std.Tactic.Lint.Basic
[192/990] Compiling Std.Linter.UnreachableTactic
[192/990] Compiling Std.Tactic.GuardExpr
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[195/990] Building Std.Data.MLList.Heartbeats
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[196/990] Building Aesop.Options.Internal
[197/990] Building Std.Lean.Meta.SavedState
[198/990] Building Std.Data.Json
[199/990] Linking Duper.Unif
[200/990] Linking Std.Data.Array.Basic
[200/990] Linking Duper.Util.Reduction
[200/990] Linking Duper.Match
[200/990] Linking Std.Lean.Meta.Basic
[200/990] Building Std.Control.ForInStep
error: > LEAN_PATH=./lake-packages/std/build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/Cli/build/lib:./lake-packages/proofwidgets/build/lib:./lake-packages/mathlib/build/lib:./lake-packages/Duper/build/lib:./lake-packages/autograder/build/lib:./build/lib LD_LIBRARY_PATH=./lake-packages/std/build/lib /usr/bin/lean -Dlinter.missingDocs=true -DwarningAsError=true ./lake-packages/std/././Std/Tactic/Relation/Symm.lean -R ./lake-packages/std/./. -o ./lake-packages/std/build/lib/Std/Tactic/Relation/Symm.olean -i ./lake-packages/std/build/lib/Std/Tactic/Relation/Symm.ilean -c ./lake-packages/std/build/ir/Std/Tactic/Relation/Symm.c
error: stdout:
./lake-packages/std/././Std/Tactic/Relation/Symm.lean:22:39: error: overloaded, errors
  failed to synthesize instance
    EmptyCollection WhnfCoreConfig

  invalid {...} notation, expected type is not of the form (C ...)
    WhnfCoreConfig
./lake-packages/std/././Std/Tactic/Relation/Symm.lean:26:43: error: application type mismatch
  Array DiscrTree.Key
argument
  DiscrTree.Key
has type
  Bool → Type : Type 1
but is expected to have type
  Type : Type 1
./lake-packages/std/././Std/Tactic/Relation/Symm.lean:26:43: error: application type mismatch
  Array DiscrTree.Key
argument
  DiscrTree.Key
has type
  Bool → Type : Type 1
but is expected to have type
  Type : Type 1
./lake-packages/std/././Std/Tactic/Relation/Symm.lean:43:8: error: failed to infer binder type
./lake-packages/std/././Std/Tactic/Relation/Symm.lean:43:8: error: don't know how to synthesize placeholder for argument 'α'
context:
decl : Name
x✝ : Syntax
kind : AttributeKind
declTy : Expr := ConstantInfo.type __do_lift✝
xs : Array Expr
fst✝ : Array BinderInfo
targetTy✝ : Expr
fail : MetaM Unit :=
  Lean.throwError
    (toMessageData "@[symm] attribute only applies to lemmas proving x ∼ y → y ∼ x, got " ++ toMessageData declTy ++
      toMessageData "")
val✝ targetTy rel arg✝¹ arg✝ : Expr
⊢ Type
./lake-packages/std/././Std/Tactic/Relation/Symm.lean:43:14: error: don't know how to synthesize implicit argument
  @withReducible MetaM (instMonadControlT_1 MetaM) instMonadMetaM
    (Array (DiscrTree.Key (?m.2770 decl x✝ kind __do_lift✝ __discr✝² xs fst✝ targetTy✝ val✝ targetTy rel arg✝¹ arg✝)))
    (liftM (DiscrTree.mkPath rel symmExt.config))
context:
decl : Name
x✝ : Syntax
kind : AttributeKind
declTy : Expr := ConstantInfo.type __do_lift✝
xs : Array Expr
fst✝ : Array BinderInfo
targetTy✝ : Expr
fail : MetaM Unit :=
  Lean.throwError
    (toMessageData "@[symm] attribute only applies to lemmas proving x ∼ y → y ∼ x, got " ++ toMessageData declTy ++
      toMessageData "")
val✝ targetTy rel arg✝¹ arg✝ : Expr
⊢ Type
./lake-packages/std/././Std/Tactic/Relation/Symm.lean:43:31: error: don't know how to synthesize implicit argument
  @DiscrTree.mkPath (?m.2770 decl x✝ kind __do_lift✝ __discr✝² xs fst✝ targetTy✝ val✝ targetTy rel arg✝¹ arg✝) rel
    symmExt.config
context:
decl : Name
x✝ : Syntax
kind : AttributeKind
declTy : Expr := ConstantInfo.type __do_lift✝
xs : Array Expr
fst✝ : Array BinderInfo
targetTy✝ : Expr
fail : MetaM Unit :=
  Lean.throwError
    (toMessageData "@[symm] attribute only applies to lemmas proving x ∼ y → y ∼ x, got " ++ toMessageData declTy ++
      toMessageData "")
val✝ targetTy rel arg✝¹ arg✝ : Expr
⊢ Bool
./lake-packages/std/././Std/Tactic/Relation/Symm.lean:76:4: error: failed to synthesize instance for 'for_in%' notation
  ForIn (ReaderT Context (StateRefT' IO.RealWorld State CoreM)) (?m.4446 tgt k rel arg✝¹ arg✝ __do_lift✝¹) ?m.5691
./lake-packages/std/././Std/Tactic/Relation/Symm.lean:76:4: error: invalid field notation, type is not of the form (C ...) where C is a constant
  r✝
has type
  ?m.4448 tgt k rel arg✝¹ arg✝ __do_lift✝¹ __do_lift✝
./lake-packages/std/././Std/Tactic/Relation/Symm.lean:76:4: error: invalid field notation, type is not of the form (C ...) where C is a constant
  r✝
has type
  ?m.4448 tgt k rel arg✝¹ arg✝ __do_lift✝¹ __do_lift✝
error: external command `/usr/bin/lean` exited with code 1
[200/990] Building Mathlib.Tactic.ToLevel
[200/990] Building Mathlib.Util.CompileInductive
[201/990] Compiling Std.Tactic.NoMatch
[206/990] Building Qq.Macro
[207/990] Linking Std.Lean.Format
[208/990] Building Std.Linter.UnnecessarySeqFocus
[209/990] Building Std.Tactic.NormCast.Ext
[210/990] Building Duper.DUnif.Utils
[211/990] Compiling Duper.Util.LazyList
[212/990] Linking Duper.Util.OccursCheck
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[214/990] Building Mathlib.Tactic.Conv
[214/990] Compiling Duper.Util.Misc
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[216/990] Building Std.Classes.Cast
[217/990] Building Std.CodeAction.Basic
[218/990] Building Std.Tactic.Lint.Frontend
[219/990] Building Mathlib.Tactic.Recover
[220/990] Building Std.Data.Char
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[221/990] Building Mathlib.Tactic.HigherOrder
[222/990] Compiling Duper.DUnif.Utils
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[223/990] Compiling Std.Data.Json
[224/990] Linking Std.Tactic.Lint.Basic
[225/990] Compiling Std.Linter.UnnecessarySeqFocus
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[226/990] Linking Std.Linter.UnreachableTactic
[226/990] Building Std.Tactic.Lint.TypeClass
[226/990] Building Std.Tactic.Lint.Misc
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[229/990] Linking Std.CodeAction.Attr
[229/990] Linking Std.Tactic.GuardExpr
[229/990] Building Std.Tactic.Lint.Simp
[230/990] Building Aesop.Options
[231/990] Linking Std.Tactic.NoMatch
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[233/990] Building Aesop.Util.EqualUpToIds
[233/990] Building Mathlib.Tactic.Replace
[234/990] Building Mathlib.Tactic.DeriveToExpr
[236/990] Linking Duper.Util.LazyList
[238/990] Building Std.Tactic.TryThis
[239/990] Linking Duper.Expr
[239/990] Building Std.Linter
[240/990] Building Mathlib.Util.Delaborators
[241/990] Building Std.Tactic.NormCast.Lemmas
[243/990] Compiling Std.Linter
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[244/990] Building Mathlib.Init.Set
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[245/990] Building Duper.DUnif.UnifProblem
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[246/990] Linking Duper.DUnif.Utils
[246/990] Building Mathlib.Tactic.ApplyCongr
[248/990] Linking Std.Data.Json
[251/990] Compiling Std.CodeAction.Basic
[251/990] Building Std.CodeAction.Deprecated
[251/990] Building Std.CodeAction.Misc
error: > LEAN_PATH=./lake-packages/std/build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/Cli/build/lib:./lake-packages/proofwidgets/build/lib:./lake-packages/mathlib/build/lib:./lake-packages/Duper/build/lib:./lake-packages/autograder/build/lib:./build/lib LD_LIBRARY_PATH=./lake-packages/std/build/lib /usr/bin/lean -Dlinter.missingDocs=true -DwarningAsError=true ./lake-packages/std/././Std/Tactic/Lint/Simp.lean -R ./lake-packages/std/./. -o ./lake-packages/std/build/lib/Std/Tactic/Lint/Simp.olean -i ./lake-packages/std/build/lib/Std/Tactic/Lint/Simp.ilean -c ./lake-packages/std/build/ir/Std/Tactic/Lint/Simp.c
error: stdout:
./lake-packages/std/././Std/Tactic/Lint/Simp.lean:81:53: error: type expected, got
  (DiscrTree α : Bool → Type)
./lake-packages/std/././Std/Tactic/Lint/Simp.lean:232:43: error: unknown identifier 'simpDtConfig'
./lake-packages/std/././Std/Tactic/Lint/Simp.lean:232:71: error: unknown identifier 'simpDtConfig'
error: external command `/usr/bin/lean` exited with code 1
[251/990] Building Std.Tactic.GuardMsgs
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[253/990] Linking Std.Linter.UnnecessarySeqFocus
[254/990] Linking Std.Linter
error: > LEAN_PATH=./lake-packages/std/build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/Cli/build/lib:./lake-packages/proofwidgets/build/lib:./lake-packages/mathlib/build/lib:./lake-packages/Duper/build/lib:./lake-packages/autograder/build/lib:./build/lib LD_LIBRARY_PATH=./lake-packages/std/build/lib /usr/bin/lean -Dlinter.missingDocs=true -DwarningAsError=true ./lake-packages/std/././Std/Tactic/TryThis.lean -R ./lake-packages/std/./. -o ./lake-packages/std/build/lib/Std/Tactic/TryThis.olean -i ./lake-packages/std/build/lib/Std/Tactic/TryThis.ilean -c ./lake-packages/std/build/ir/Std/Tactic/TryThis.c
error: stdout:
./lake-packages/std/././Std/Tactic/TryThis.lean:105:43: error: invalid field 'versionedIdentifier', the environment does not contain 'Lean.Server.FileWorker.EditableDocument.versionedIdentifier'
  doc
has type
  FileWorker.EditableDocument
error: external command `/usr/bin/lean` exited with code 1
[258/990] Compiling Std.Tactic.Lint.Misc
error: > LEAN_PATH=./lake-packages/std/build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/Cli/build/lib:./lake-packages/proofwidgets/build/lib:./lake-packages/mathlib/build/lib:./lake-packages/Duper/build/lib:./lake-packages/autograder/build/lib:./build/lib LD_LIBRARY_PATH=./lake-packages/std/build/lib /usr/bin/lean -Dlinter.missingDocs=true -DwarningAsError=true ./lake-packages/std/././Std/CodeAction/Deprecated.lean -R ./lake-packages/std/./. -o ./lake-packages/std/build/lib/Std/CodeAction/Deprecated.olean -i ./lake-packages/std/build/lib/Std/CodeAction/Deprecated.ilean -c ./lake-packages/std/build/ir/Std/CodeAction/Deprecated.c
error: stdout:
./lake-packages/std/././Std/CodeAction/Deprecated.lean:63:39: error: invalid field 'versionedIdentifier', the environment does not contain 'Lean.Server.FileWorker.EditableDocument.versionedIdentifier'
  doc
has type
  FileWorker.EditableDocument
error: external command `/usr/bin/lean` exited with code 1
error: > LEAN_PATH=./lake-packages/std/build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/Cli/build/lib:./lake-packages/proofwidgets/build/lib:./lake-packages/mathlib/build/lib:./lake-packages/Duper/build/lib:./lake-packages/autograder/build/lib:./build/lib LD_LIBRARY_PATH=./lake-packages/std/build/lib /usr/bin/lean -Dlinter.missingDocs=true -DwarningAsError=true ./lake-packages/std/././Std/Tactic/GuardMsgs.lean -R ./lake-packages/std/./. -o ./lake-packages/std/build/lib/Std/Tactic/GuardMsgs.olean -i ./lake-packages/std/build/lib/Std/Tactic/GuardMsgs.ilean -c ./lake-packages/std/build/ir/Std/Tactic/GuardMsgs.c
error: stdout:
./lake-packages/std/././Std/Tactic/GuardMsgs.lean:190:36: error: invalid field 'versionedIdentifier', the environment does not contain 'Lean.Server.FileWorker.EditableDocument.versionedIdentifier'
  doc
has type
  FileWorker.EditableDocument
error: external command `/usr/bin/lean` exited with code 1
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[259/990] Linking Std.CodeAction.Basic
error: > LEAN_PATH=./lake-packages/std/build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/Cli/build/lib:./lake-packages/proofwidgets/build/lib:./lake-packages/mathlib/build/lib:./lake-packages/Duper/build/lib:./lake-packages/autograder/build/lib:./build/lib LD_LIBRARY_PATH=./lake-packages/std/build/lib /usr/bin/lean -Dlinter.missingDocs=true -DwarningAsError=true ./lake-packages/std/././Std/CodeAction/Misc.lean -R ./lake-packages/std/./. -o ./lake-packages/std/build/lib/Std/CodeAction/Misc.olean -i ./lake-packages/std/build/lib/Std/CodeAction/Misc.ilean -c ./lake-packages/std/build/ir/Std/CodeAction/Misc.c
error: stdout:
./lake-packages/std/././Std/CodeAction/Misc.lean:88:37: error: invalid field 'versionedIdentifier', the environment does not contain 'Lean.Server.FileWorker.EditableDocument.versionedIdentifier'
  doc
has type
  FileWorker.EditableDocument
./lake-packages/std/././Std/CodeAction/Misc.lean:159:36: error: invalid field 'versionedIdentifier', the environment does not contain 'Lean.Server.FileWorker.EditableDocument.versionedIdentifier'
  doc
has type
  FileWorker.EditableDocument
./lake-packages/std/././Std/CodeAction/Misc.lean:174:38: error: invalid field 'versionedIdentifier', the environment does not contain 'Lean.Server.FileWorker.EditableDocument.versionedIdentifier'
  doc
has type
  FileWorker.EditableDocument
./lake-packages/std/././Std/CodeAction/Misc.lean:206:32: error: invalid field 'versionedIdentifier', the environment does not contain 'Lean.Server.FileWorker.EditableDocument.versionedIdentifier'
  doc
has type
  FileWorker.EditableDocument
./lake-packages/std/././Std/CodeAction/Misc.lean:305:36: error: invalid field 'versionedIdentifier', the environment does not contain 'Lean.Server.FileWorker.EditableDocument.versionedIdentifier'
  doc
has type
  FileWorker.EditableDocument
./lake-packages/std/././Std/CodeAction/Misc.lean:362:36: error: invalid field 'versionedIdentifier', the environment does not contain 'Lean.Server.FileWorker.EditableDocument.versionedIdentifier'
  doc
has type
  FileWorker.EditableDocument
error: external command `/usr/bin/lean` exited with code 1
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[262/990] Linking Std.Tactic.Lint.Misc
stdout:
./lake-packages/Duper/././Duper/DUnif/UnifProblem.lean:324:15: warning: unused variable `a` [linter.unusedVariables]
[264/990] Compiling Duper.DUnif.UnifProblem
[265/990] Building Mathlib.Tactic.ToExpr
[266/990] Building Mathlib.Tactic.FBinop
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[268/990] Linking Duper.DUnif.UnifProblem
[269/990] Building Duper.DUnif.Oracles
[270/990] Building Mathlib.Data.SProd
[272/990] Building Qq.Delab
[273/990] Compiling Duper.DUnif.Oracles
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[274/990] Linking Duper.Util.Misc
[275/990] Building Duper.Util.AbstractMVars
[275/990] Building Duper.Order
[275/990] Building Duper.DUnif.Bindings
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[276/990] Linking Duper.DUnif.Oracles
[278/990] Building Qq.MetaM
[279/990] Building Qq.AssertInstancesCommute
[279/990] Building Qq.Match
[280/990] Compiling Duper.Util.AbstractMVars
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[282/990] Linking Duper.Util.AbstractMVars
stdout:
./lake-packages/Duper/././Duper/DUnif/Bindings.lean:317:52: warning: unused variable `β` [linter.unusedVariables]
./lake-packages/Duper/././Duper/DUnif/Bindings.lean:317:97: warning: unused variable `δ` [linter.unusedVariables]
[284/990] Compiling Duper.DUnif.Bindings
stdout:
./lake-packages/Duper/././Duper/Order.lean:350:26: warning: unused variable `n` [linter.unusedVariables]
./lake-packages/Duper/././Duper/Order.lean:361:12: warning: unused variable `n` [linter.unusedVariables]
./lake-packages/Duper/././Duper/Order.lean:441:23: warning: unused variable `symbolPrecMap` [linter.unusedVariables]
./lake-packages/Duper/././Duper/Order.lean:441:55: warning: unused variable `highesetPrecSymbolHasArityZero` [linter.unusedVariables]
[285/990] Compiling Duper.Order
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[286/990] Linking Duper.DUnif.Bindings
[287/990] Building Duper.DUnif.UnifRules
[288/990] Building Qq
[289/990] Building Mathlib.Util.Qq
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[291/990] Linking Duper.Order
[292/990] Building Duper.Clause
[293/990] Compiling Duper.DUnif.UnifRules
stdout:
./lake-packages/Duper/././Duper/Clause.lean:310:20: warning: unused variable `instMonad` [linter.unusedVariables]
[294/990] Compiling Duper.Clause
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[295/990] Linking Duper.DUnif.UnifRules
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[297/990] Linking Duper.Clause
[298/990] Building Duper.MClause
[299/990] Compiling Duper.MClause
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[300/990] Linking Duper.MClause
[301/990] Building Duper.Util.DeeplyOccurringVars
stdout:
./lake-packages/Duper/././Duper/Util/DeeplyOccurringVars.lean:16:21: warning: unused variable `ty` [linter.unusedVariables]
./lake-packages/Duper/././Duper/Util/DeeplyOccurringVars.lean:17:17: warning: unused variable `ty` [linter.unusedVariables]
./lake-packages/Duper/././Duper/Util/DeeplyOccurringVars.lean:21:18: warning: unused variable `t` [linter.unusedVariables]
[302/990] Compiling Duper.Util.DeeplyOccurringVars
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[303/990] Linking Duper.Util.DeeplyOccurringVars

math2001 $
hrmacbeth commented 6 months ago

Unfortunately I haven't been able to reproduce this, and I got a colleague to try out a fresh install on his computer, which also didn't reproduce this. I'm guessing the issue is this pervasive

cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done

I recommend asking about the issue on the Lean Zulip in #new members.

tydeu commented 6 months ago

Thanks for the report!

To get going, it should be enough to run lake build Library; this is what's done in the Gitpod init script.

I'll look into fixing the lakefile so that lake build does that automatically, and into fixing the Std build error you report.

To achieve this, you can move the @[default_target] from lean_lib Math2001 to lean_lib Library. 😄

hrmacbeth commented 6 months ago

@arbitrary-dev I have updated the lakefile so that lake build is valid, and bumped the repo to depend on the latest stable Mathlib. It might be worth trying again on the new version. If your errors persist, feel free to ask for real-time help on the Lean Zulip.

arbitrary-dev commented 5 months ago

Okay, it seems to be working now, with a little bit of trickery...

$ lean --version
Lean (version 4.2.0, Release)

$ git log
commit 7bc1e7af336e8c7e89585dee179a4e32766c300e (grafted, HEAD -> main, origin/main,>
Author: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Date:   Mon Jan 8 21:56:15 2024 -0500

    Update Mon Jan  8 21:56:15 EST 2024

$ lake exe cache get
warning: improperly formatted manifest: manifest version `7` is higher than this Lake's '6'; you may need to update your `lean-toolchain`
error: missing manifest; use `lake update` to generate one

$ lake build
warning: improperly formatted manifest: manifest version `7` is higher than this Lake's '6'; you may need to update your `lean-toolchain`
error: missing manifest; use `lake update` to generate one

$ lake update
cloning https://github.com/leanprover-community/mathlib4 to ./lake-packages/mathlib
cloning https://github.com/hrmacbeth/duper to ./lake-packages/Duper
cloning https://github.com/robertylewis/lean4-autograder-main to ./lake-packages/autograder
cloning https://github.com/leanprover-community/quote4 to ./lake-packages/Qq
cloning https://github.com/leanprover/lean4-cli to ./lake-packages/Cli
cloning https://github.com/leanprover-community/ProofWidgets4 to ./lake-packages/proofwidgets
cloning https://github.com/leanprover/std4 to ./lake-packages/std
cloning https://github.com/leanprover-community/aesop to ./lake-packages/aesop
warning: improperly formatted manifest: manifest version `7` is higher than this Lake's '6'; you may need to update your `lean-toolchain`

$ lake exe cache get
info: [0/9] Fetching proofwidgets cloud release
info: [1/9] Building Cache.IO
info: [2/9] Compiling Cache.IO
info: [2/9] Building Cache.Hashing
info: [3/9] Compiling Cache.Hashing
info: [3/9] Building Cache.Requests
info: stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
info: [5/9] Compiling Cache.Requests
info: [5/9] Building Cache.Main
info: [6/9] Compiling Cache.Main
info: stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
info: stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
info: stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
info: [9/9] Linking cache
Dependency Mathlib uses a different lean-toolchain
  Project uses leanprover/lean4:v4.3.0
  Mathlib uses leanprover/lean4:v4.2.0

The cache will not work unless your project's toolchain matches Mathlib's toolchain
This can be achieved by copying the contents of the file `lake-packages/mathlib/lean-toolchain`
into the `lean-toolchain` file at the root directory of your project
You can use `cp lake-packages/mathlib/lean-toolchain ./lean-toolchain`

$ cp lake-packages/mathlib/lean-toolchain lean-toolchain

$ lake exe cache get
Attempting to download 3875 file(s)
Downloaded: 3875 file(s) [attempted 3875/3875 = 100%] (100% success)
Decompressing 3875 file(s)
unpacked in 5140 ms

$ lake build
[1/29] Building Mathlib.Init.Data.Nat.Notation
[1/29] Building Std.Util.ExtendedBinder
[1/30] Building Std.Data.Option.Init.Lemmas
[1/33] Building Std.Lean.Command
[1/33] Building Std.Tactic.HaveI
[1/33] Building Std.Tactic.Unreachable
[1/33] Building Std.Tactic.OpenPrivate
[1/35] Building Std.Lean.TagAttribute
[1/40] Building Std.Util.TermUnsafe
[1/40] Building Std.Tactic.ByCases
[1/40] Building Std.Tactic.SeqFocus
[1/41] Building Std.Lean.Name
[1/49] Building Std.Lean.Float
[1/85] Building Std.Lean.Tactic
[1/92] Building Std.Lean.NameMapAttribute
[1/89] Building Std.Lean.Position
[2/1092] Building Std.Data.Ord
[3/1092] Building Std.Lean.Parser
[4/1092] Compiling Std.Lean.Name
stderr:
cc: warning: /usr/lib64/libgmp.so: linker input file unused because linking not done
[5/1092] Building Std.Data.Fin.Init.Lemmas
[6/1092] Compiling Std.Lean.TagAttribute
[7/1092] Building Std.Lean.Meta.Basic
[8/1092] Compiling Std.Lean.Tactic
[9/1092] Compiling Std.Lean.Position
...
[1075/1092] Building Math2001.Homework.hw10
stdout:
./././Math2001/04_Proofs_with_Structure_II/03_Exists_Unique.lean:23:0: warning: declaration uses 'sorry'
./././Math2001/04_Proofs_with_Structure_II/03_Exists_Unique.lean:72:0: warning: declaration uses 'sorry'
./././Math2001/04_Proofs_with_Structure_II/03_Exists_Unique.lean:75:0: warning: declaration uses 'sorry'
./././Math2001/04_Proofs_with_Structure_II/03_Exists_Unique.lean:78:0: warning: declaration uses 'sorry'
error: > LEAN_PATH=./lake-packages/std/build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/Cli/build/lib:./lake-packages/proofwidgets/build/lib:./lake-packages/mathlib/build/lib:./lake-packages/Duper/build/lib:./lake-packages/autograder/build/lib:./build/lib LD_LIBRARY_PATH=./lake-packages/std/build/lib:./lake-packages/Duper/build/lib:./build/lib /usr/bin/lean -Dlinter.unusedVariables=false -DquotPrecheck=false -DwarningAsError=false -Dpp.unicode.fun=true ./././Math2001/08_Functions/03_Composition.lean -R ././. -o ./build/lib/Math2001/08_Functions/03_Composition.olean -i ./build/lib/Math2001/08_Functions/03_Composition.ilean -c ./build/ir/Math2001/08_Functions/03_Composition.c --load-dynlib=./lake-packages/std/build/lib/libStd-Data-Ord-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Lean-Meta-LCtx-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Lean-Parser-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Tactic-OpenPrivate-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Tactic-Simpa-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Classes-Order-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Control-ForInStep-Basic-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Lean-Command-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Tactic-Unreachable-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Linter-UnreachableTactic-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Lean-TagAttribute-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Lean-AttributeExtra-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Linter-UnnecessarySeqFocus-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Linter-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Tactic-NoMatch-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Util-TermUnsafe-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Tactic-GuardExpr-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Tactic-ByCases-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Tactic-SeqFocus-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Lean-Name-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Lean-Format-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Lean-Position-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Lean-Float-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Lean-Json-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Data-Json-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Tactic-TryThis-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Tactic-ShowTerm-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Tactic-SimpTrace-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Lean-Meta-Basic-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Lean-Tactic-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Tactic-Basic-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Lean-NameMapAttribute-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Tactic-Lint-Basic-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Data-Fin-Init-Lemmas-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Data-List-Init-Lemmas-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Data-Array-Init-Basic-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Data-Array-Basic-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Tactic-Lint-Misc-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Logic-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Data-Nat-Init-Lemmas-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Classes-Dvd-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Data-Nat-Basic-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Data-Nat-Lemmas-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Data-BinomialHeap-Basic-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Data-BinomialHeap-Lemmas-1.so --load-dynlib=./lake-packages/std/build/lib/libStd-Data-BinomialHeap-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Util-IdStrategyHeap-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Util-Misc-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Expr-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Util-Reduction-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Order-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Clause-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Util-MessageData-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Util-LazyList-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-DUnif-UnifProblem-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Util-OccursCheck-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-DUnif-Utils-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-DUnif-Bindings-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-DUnif-Oracles-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-DUnif-UnifRules-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Unif-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-MClause-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Match-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Util-AbstractMVars-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-RuleM-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Selection-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Fingerprint-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-SubsumptionTrie-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Util-ClauseSubsumptionCheck-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Util-StrategyHeap-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Util-DeeplyOccurringVars-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-ProverM-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-ClauseStreamHeap-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Simp-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Util-ProofReconstruction-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Rules-Clausification-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Preprocessing-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Rules-ClauseSubsumption-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Rules-ContextualLiteralCutting-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Rules-Demodulation-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Rules-EqualitySubsumption-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Rules-SimplifyReflect-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-BackwardSimplification-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Rules-BetaEtaReduction-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Rules-BoolSimp-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Rules-ClausifyPropEq-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Rules-ElimDupLit-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Rules-ElimResolvedLit-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Rules-EqualityFactoring-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Rules-EqualityResolution-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Rules-FalseElim-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Rules-IdentBoolFalseElim-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Rules-IdentPropFalseElim-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Rules-Superposition-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Rules-SyntacticTautologyDeletion1-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Rules-SyntacticTautologyDeletion2-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Rules-SyntacticTautologyDeletion3-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Rules-DestructiveEqualityResolution-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Rules-IdentBoolHoist-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Rules-BoolHoist-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Rules-EqHoist-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Rules-ExistsHoist-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Rules-ForallHoist-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Rules-NeHoist-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Rules-ArgumentCongruence-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Rules-FluidSup-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Rules-FluidBoolHoist-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Util-TypeInhabitationReasoning-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Saturate-1.so --load-dynlib=./lake-packages/Duper/build/lib/libDuper-Tactic-1.so
...

At least I can now error check the code.

hrmacbeth commented 5 months ago

Note:

Ah! The issue is that you should not be running lake update. Lean projects typically come with a particular version of mathlib which they are pinned to, and are unlikely to work on other versions. Have you tried the following sequence (without lake update):

git clone https://github.com/hrmacbeth/math2001.git
cd math2001
lake exe cache get
lake build Library
arbitrary-dev commented 5 months ago

As you can see from the log provided, neither lake exe cache get nor lake build worked for me until I called lake update first on a latest version of your project.

hrmacbeth commented 5 months ago

Nonetheless, you should certainly expect that lake update will break a project. Can you try elan self update before the other commands? Otherwise maybe @tydeu has ideas.

tydeu commented 5 months ago

@arbitrary-dev From your log, the problem you had appears to be that your lean --version was at 4.2.0, when this repository was at 4.3.0. It is not clear to me why this was the case. Maybe you had an Elan override set? (You can check with elan override list and/or elan show.)

arbitrary-dev commented 5 months ago

I have lean provided to me by my OS repository...

$ elan show
zsh: command not found: elan

$ equery l lean
 * Searching for lean ...
[IP-] [  ] sci-mathematics/lean-4.2.0_rc4:0/4
hrmacbeth commented 5 months ago

That'll be the problem then! A standard install of Lean will include elan, which silently manages Lean versions for you. You should either get a standard install, or manually install 4.3.0.

hrmacbeth commented 5 months ago

See discussion of the problem.