chore: test for issue #4064

closes #4064
chore: update stage0
2026-03-21 12:24:11 +00:00 · 2024-05-06 15:55:07 -07:00 · 2024-05-06 15:50:18 -07:00
168 changed files with 11 additions and 0 deletions
--- a/stage0/src/CMakeLists.txt
+++ b/stage0/src/CMakeLists.txt
--- a/stage0/src/kernel/declaration.cpp
+++ b/stage0/src/kernel/declaration.cpp
--- a/stage0/src/kernel/declaration.h
+++ b/stage0/src/kernel/declaration.h
--- a/stage0/src/kernel/environment.cpp
+++ b/stage0/src/kernel/environment.cpp
--- a/stage0/src/kernel/environment.h
+++ b/stage0/src/kernel/environment.h
--- a/stage0/src/kernel/inductive.cpp
+++ b/stage0/src/kernel/inductive.cpp
--- a/stage0/src/kernel/type_checker.cpp
+++ b/stage0/src/kernel/type_checker.cpp
--- a/stage0/src/kernel/type_checker.h
+++ b/stage0/src/kernel/type_checker.h
--- a/stage0/src/library/compiler/ir_interpreter.cpp
+++ b/stage0/src/library/compiler/ir_interpreter.cpp
--- a/stage0/src/runtime/process.cpp
+++ b/stage0/src/runtime/process.cpp
--- a/stage0/stdlib/Init/Control/Lawful/Basic.c
+++ b/stage0/stdlib/Init/Control/Lawful/Basic.c
--- a/stage0/stdlib/Init/Core.c
+++ b/stage0/stdlib/Init/Core.c
--- a/stage0/stdlib/Init/Data/Array/Basic.c
+++ b/stage0/stdlib/Init/Data/Array/Basic.c
--- a/stage0/stdlib/Init/Data/Array/Lemmas.c
+++ b/stage0/stdlib/Init/Data/Array/Lemmas.c
--- a/stage0/stdlib/Init/Data/Array/Mem.c
+++ b/stage0/stdlib/Init/Data/Array/Mem.c
--- a/stage0/stdlib/Init/Data/List.c
+++ b/stage0/stdlib/Init/Data/List.c
--- a/stage0/stdlib/Init/Data/List/BasicAux.c
+++ b/stage0/stdlib/Init/Data/List/BasicAux.c
--- a/stage0/stdlib/Init/Data/List/Impl.c
+++ b/stage0/stdlib/Init/Data/List/Impl.c
--- a/stage0/stdlib/Init/Data/List/Lemmas.c
+++ b/stage0/stdlib/Init/Data/List/Lemmas.c
--- a/stage0/stdlib/Init/Data/List/TakeDrop.c
+++ b/stage0/stdlib/Init/Data/List/TakeDrop.c
--- a/stage0/stdlib/Init/Data/String/Basic.c
+++ b/stage0/stdlib/Init/Data/String/Basic.c
--- a/stage0/stdlib/Init/Data/String/Extra.c
+++ b/stage0/stdlib/Init/Data/String/Extra.c
--- a/stage0/stdlib/Init/Meta.c
+++ b/stage0/stdlib/Init/Meta.c
--- a/stage0/stdlib/Init/Notation.c
+++ b/stage0/stdlib/Init/Notation.c
--- a/stage0/stdlib/Init/Prelude.c
+++ b/stage0/stdlib/Init/Prelude.c
--- a/stage0/stdlib/Init/System/IO.c
+++ b/stage0/stdlib/Init/System/IO.c
--- a/stage0/stdlib/Init/Tactics.c
+++ b/stage0/stdlib/Init/Tactics.c
--- a/stage0/stdlib/Init/WFTactics.c
+++ b/stage0/stdlib/Init/WFTactics.c
--- a/stage0/stdlib/Lean/BuiltinDocAttr.c
+++ b/stage0/stdlib/Lean/BuiltinDocAttr.c
--- a/stage0/stdlib/Lean/Compiler/ExternAttr.c
+++ b/stage0/stdlib/Lean/Compiler/ExternAttr.c
--- a/stage0/stdlib/Lean/Compiler/IR/Basic.c
+++ b/stage0/stdlib/Lean/Compiler/IR/Basic.c
--- a/stage0/stdlib/Lean/Compiler/IR/RC.c
+++ b/stage0/stdlib/Lean/Compiler/IR/RC.c
--- a/stage0/stdlib/Lean/Compiler/IR/ResetReuse.c
+++ b/stage0/stdlib/Lean/Compiler/IR/ResetReuse.c
--- a/stage0/stdlib/Lean/Compiler/InitAttr.c
+++ b/stage0/stdlib/Lean/Compiler/InitAttr.c
--- a/stage0/stdlib/Lean/Compiler/LCNF/AuxDeclCache.c
+++ b/stage0/stdlib/Lean/Compiler/LCNF/AuxDeclCache.c
--- a/stage0/stdlib/Lean/Compiler/LCNF/Basic.c
+++ b/stage0/stdlib/Lean/Compiler/LCNF/Basic.c
--- a/stage0/stdlib/Lean/Compiler/LCNF/Closure.c
+++ b/stage0/stdlib/Lean/Compiler/LCNF/Closure.c
--- a/stage0/stdlib/Lean/Compiler/LCNF/FloatLetIn.c
+++ b/stage0/stdlib/Lean/Compiler/LCNF/FloatLetIn.c
--- a/stage0/stdlib/Lean/Compiler/LCNF/JoinPoints.c
+++ b/stage0/stdlib/Lean/Compiler/LCNF/JoinPoints.c
--- a/stage0/stdlib/Lean/Compiler/LCNF/Main.c
+++ b/stage0/stdlib/Lean/Compiler/LCNF/Main.c
--- a/stage0/stdlib/Lean/Compiler/LCNF/PassManager.c
+++ b/stage0/stdlib/Lean/Compiler/LCNF/PassManager.c
--- a/stage0/stdlib/Lean/Compiler/LCNF/Passes.c
+++ b/stage0/stdlib/Lean/Compiler/LCNF/Passes.c
--- a/stage0/stdlib/Lean/Compiler/LCNF/PhaseExt.c
+++ b/stage0/stdlib/Lean/Compiler/LCNF/PhaseExt.c
--- a/stage0/stdlib/Lean/Compiler/LCNF/PrettyPrinter.c
+++ b/stage0/stdlib/Lean/Compiler/LCNF/PrettyPrinter.c
--- a/stage0/stdlib/Lean/Compiler/LCNF/Simp/JpCases.c
+++ b/stage0/stdlib/Lean/Compiler/LCNF/Simp/JpCases.c
--- a/stage0/stdlib/Lean/Compiler/LCNF/Simp/Main.c
+++ b/stage0/stdlib/Lean/Compiler/LCNF/Simp/Main.c
--- a/stage0/stdlib/Lean/Compiler/LCNF/Simp/SimpM.c
+++ b/stage0/stdlib/Lean/Compiler/LCNF/Simp/SimpM.c
--- a/stage0/stdlib/Lean/Compiler/LCNF/Specialize.c
+++ b/stage0/stdlib/Lean/Compiler/LCNF/Specialize.c
--- a/stage0/stdlib/Lean/Compiler/LCNF/Testing.c
+++ b/stage0/stdlib/Lean/Compiler/LCNF/Testing.c
--- a/stage0/stdlib/Lean/Compiler/Main.c
+++ b/stage0/stdlib/Lean/Compiler/Main.c
--- a/stage0/stdlib/Lean/CoreM.c
+++ b/stage0/stdlib/Lean/CoreM.c
--- a/stage0/stdlib/Lean/Data/HashMap.c
+++ b/stage0/stdlib/Lean/Data/HashMap.c
--- a/stage0/stdlib/Lean/Data/Lsp/Capabilities.c
+++ b/stage0/stdlib/Lean/Data/Lsp/Capabilities.c
--- a/stage0/stdlib/Lean/Data/Lsp/LanguageFeatures.c
+++ b/stage0/stdlib/Lean/Data/Lsp/LanguageFeatures.c
--- a/stage0/stdlib/Lean/Declaration.c
+++ b/stage0/stdlib/Lean/Declaration.c
--- a/stage0/stdlib/Lean/Elab/App.c
+++ b/stage0/stdlib/Lean/Elab/App.c
--- a/stage0/stdlib/Lean/Elab/Binders.c
+++ b/stage0/stdlib/Lean/Elab/Binders.c
--- a/stage0/stdlib/Lean/Elab/BuiltinNotation.c
+++ b/stage0/stdlib/Lean/Elab/BuiltinNotation.c
--- a/stage0/stdlib/Lean/Elab/BuiltinTerm.c
+++ b/stage0/stdlib/Lean/Elab/BuiltinTerm.c
--- a/stage0/stdlib/Lean/Elab/Command.c
+++ b/stage0/stdlib/Lean/Elab/Command.c
--- a/stage0/stdlib/Lean/Elab/DefView.c
+++ b/stage0/stdlib/Lean/Elab/DefView.c
--- a/stage0/stdlib/Lean/Elab/Deriving/BEq.c
+++ b/stage0/stdlib/Lean/Elab/Deriving/BEq.c
--- a/stage0/stdlib/Lean/Elab/Deriving/DecEq.c
+++ b/stage0/stdlib/Lean/Elab/Deriving/DecEq.c
--- a/stage0/stdlib/Lean/Elab/Deriving/FromToJson.c
+++ b/stage0/stdlib/Lean/Elab/Deriving/FromToJson.c
--- a/stage0/stdlib/Lean/Elab/Deriving/Hashable.c
+++ b/stage0/stdlib/Lean/Elab/Deriving/Hashable.c
--- a/stage0/stdlib/Lean/Elab/Deriving/Inhabited.c
+++ b/stage0/stdlib/Lean/Elab/Deriving/Inhabited.c
--- a/stage0/stdlib/Lean/Elab/Deriving/Ord.c
+++ b/stage0/stdlib/Lean/Elab/Deriving/Ord.c
--- a/stage0/stdlib/Lean/Elab/Deriving/Repr.c
+++ b/stage0/stdlib/Lean/Elab/Deriving/Repr.c
--- a/stage0/stdlib/Lean/Elab/GuardMsgs.c
+++ b/stage0/stdlib/Lean/Elab/GuardMsgs.c
--- a/stage0/stdlib/Lean/Elab/Inductive.c
+++ b/stage0/stdlib/Lean/Elab/Inductive.c
--- a/stage0/stdlib/Lean/Elab/InfoTree/Main.c
+++ b/stage0/stdlib/Lean/Elab/InfoTree/Main.c
--- a/stage0/stdlib/Lean/Elab/Match.c
+++ b/stage0/stdlib/Lean/Elab/Match.c
--- a/stage0/stdlib/Lean/Elab/MutualDef.c
+++ b/stage0/stdlib/Lean/Elab/MutualDef.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/Eqns.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/Eqns.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/Structural/BRecOn.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/Structural/BRecOn.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/Structural/Eqns.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/Structural/Eqns.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/Structural/IndPred.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/Structural/IndPred.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/Structural/SmartUnfolding.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/Structural/SmartUnfolding.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/WF/Eqns.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/WF/Eqns.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/WF/GuessLex.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/WF/GuessLex.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/WF/PackMutual.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/WF/PackMutual.c
--- a/stage0/stdlib/Lean/Elab/Structure.c
+++ b/stage0/stdlib/Lean/Elab/Structure.c
--- a/stage0/stdlib/Lean/Elab/Syntax.c
+++ b/stage0/stdlib/Lean/Elab/Syntax.c
--- a/stage0/stdlib/Lean/Elab/Tactic/Basic.c
+++ b/stage0/stdlib/Lean/Elab/Tactic/Basic.c
--- a/stage0/stdlib/Lean/Elab/Tactic/BuiltinTactic.c
+++ b/stage0/stdlib/Lean/Elab/Tactic/BuiltinTactic.c
--- a/stage0/stdlib/Lean/Elab/Tactic/Conv/Pattern.c
+++ b/stage0/stdlib/Lean/Elab/Tactic/Conv/Pattern.c
--- a/stage0/stdlib/Lean/Elab/Tactic/Conv/Simp.c
+++ b/stage0/stdlib/Lean/Elab/Tactic/Conv/Simp.c
--- a/stage0/stdlib/Lean/Elab/Tactic/Ext.c
+++ b/stage0/stdlib/Lean/Elab/Tactic/Ext.c
--- a/stage0/stdlib/Lean/Elab/Tactic/NormCast.c
+++ b/stage0/stdlib/Lean/Elab/Tactic/NormCast.c
--- a/stage0/stdlib/Lean/Elab/Tactic/RCases.c
+++ b/stage0/stdlib/Lean/Elab/Tactic/RCases.c
--- a/stage0/stdlib/Lean/Elab/Tactic/Simp.c
+++ b/stage0/stdlib/Lean/Elab/Tactic/Simp.c
--- a/stage0/stdlib/Lean/Elab/Tactic/SimpTrace.c
+++ b/stage0/stdlib/Lean/Elab/Tactic/SimpTrace.c
--- a/stage0/stdlib/Lean/Elab/Tactic/Simpa.c
+++ b/stage0/stdlib/Lean/Elab/Tactic/Simpa.c
--- a/stage0/stdlib/Lean/Elab/Tactic/Simproc.c
+++ b/stage0/stdlib/Lean/Elab/Tactic/Simproc.c
--- a/stage0/stdlib/Lean/Elab/Term.c
+++ b/stage0/stdlib/Lean/Elab/Term.c
--- a/stage0/stdlib/Lean/Environment.c
+++ b/stage0/stdlib/Lean/Environment.c
--- a/stage0/stdlib/Lean/KeyedDeclsAttribute.c
+++ b/stage0/stdlib/Lean/KeyedDeclsAttribute.c
--- a/stage0/stdlib/Lean/Linter/MissingDocs.c
+++ b/stage0/stdlib/Lean/Linter/MissingDocs.c
--- a/stage0/stdlib/Lean/Linter/UnusedVariables.c
+++ b/stage0/stdlib/Lean/Linter/UnusedVariables.c
--- a/stage0/stdlib/Lean/LocalContext.c
+++ b/stage0/stdlib/Lean/LocalContext.c
--- a/Show More
+++ b/Show More
Author	SHA1	Message	Date
Leonardo de Moura	433bc1d382	chore: test for issue #4064 closes #4064	2024-05-06 15:55:07 -07:00
Leonardo de Moura	37f97a4a0d	chore: update stage0	2024-05-06 15:50:18 -07:00