Merge remote-tracking branch 'origin/main' into dev

leanprover-community · Jul 20, 2024 · a1bec2f · a1bec2f
2 parents d800617 + d53f474
commit a1bec2f
Show file tree

Hide file tree

Showing 7 changed files with 32 additions and 31 deletions.
diff --git a/Duper/Interface.lean b/Duper/Interface.lean
@@ -328,7 +328,7 @@ def addSkolemSorry : CoreM Name := do
   let opaqueVal : OpaqueVal := {name := name, levelParams := [vlvlName, ulvlName],
                                 type := type, value := term, isUnsafe := true, all := [name]}
   let decl : Declaration := (.opaqueDecl opaqueVal)
-  match (← getEnv).addDecl decl with
+  match (← getEnv).addDecl (← getOptions) decl with
   | Except.ok    env => setEnv env
   | Except.error ex  => throwKernelException ex
   return name

diff --git a/Duper/Saturate.lean b/Duper/Saturate.lean
@@ -73,7 +73,7 @@ def forwardSimpRules : ProverM (Array SimpRule) := do
       identBoolFalseElim.toSimpRule,
       datatypeDistinctness.toSimpRule, -- Inductive datatype rule
       datatypeInjectivity.toSimpRule, -- Inductive datatype rule
-      datatypeAcyclicity.toSimpRule, -- Inductive datatype rule
+      -- datatypeAcyclicity.toSimpRule, -- Inductive datatype rule
       decElim.toSimpRule,
       (forwardDemodulation (← getDemodSidePremiseIdx)).toSimpRule,
       (forwardClauseSubsumption subsumptionTrie).toSimpRule,
@@ -98,7 +98,7 @@ def forwardSimpRules : ProverM (Array SimpRule) := do
       identBoolFalseElim.toSimpRule,
       datatypeDistinctness.toSimpRule, -- Inductive datatype rule
       datatypeInjectivity.toSimpRule, -- Inductive datatype rule
-      datatypeAcyclicity.toSimpRule, -- Inductive datatype rule
+      -- datatypeAcyclicity.toSimpRule, -- Inductive datatype rule
       (forwardDemodulation (← getDemodSidePremiseIdx)).toSimpRule,
       (forwardClauseSubsumption subsumptionTrie).toSimpRule,
       (forwardEqualitySubsumption subsumptionTrie).toSimpRule,

diff --git a/Duper/Tactic.lean b/Duper/Tactic.lean
@@ -97,7 +97,7 @@ where elabFactAux (stx : Term) : TacticM (Expr × Expr × Array Name) :=
   -- elaborate term as much as possible and abstract any remaining mvars:
   Term.withoutModifyingElabMetaStateWithInfo <| withRef stx <| Term.withoutErrToSorry do
     let e ← Term.elabTerm stx none
-    Term.synthesizeSyntheticMVars (mayPostpone := false) (ignoreStuckTC := true)
+    Term.synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := true)
     let e ← instantiateMVars e
     let abstres ← Duper.abstractMVars e
     let e := abstres.expr

diff --git a/Main.lean b/Main.lean
@@ -36,28 +36,29 @@ def runDuperOnTPTP (fileName : String) (formulas : List (Expr × Expr × Array N
 
 def run (path : String) (github : Bool) : MetaM Unit := do
   let env ← getEnv
+  let opts ← getOptions
   let prop := mkSort levelZero
   let type := mkSort levelOne
   let sortu := mkSort (.param `u)
   let sortu1 := mkSort (.param `u1)
   let sortu2 := mkSort (.param `u2)
-  let env ← ofExceptKernelException $ env.addDecl (.axiomDecl {name := `Nat, levelParams := [], type := type, isUnsafe := false})
-  let env ← ofExceptKernelException $ env.addDecl (.axiomDecl {name := `Iota, levelParams := [], type := type, isUnsafe := false})
-  let env ← ofExceptKernelException $ env.addDecl (.axiomDecl {name := `Bool, levelParams := [], type := type, isUnsafe := false})
-  let env ← ofExceptKernelException $ env.addDecl (.axiomDecl {name := `Bool.false, levelParams := [], type := mkConst `Bool, isUnsafe := false})
-  let env ← ofExceptKernelException $ env.addDecl (.axiomDecl {name := `sorryAx, levelParams := [`u], type := mkForall `α .default sortu $ mkForall `synthetic .default (mkConst `Bool) $ mkBVar 1, isUnsafe := false})
-  let env ← ofExceptKernelException $ env.addDecl (.axiomDecl {name := `Eq, levelParams := [`u], type := mkForall `α .implicit sortu $ ← mkArrow (mkBVar 0) $ ← mkArrow (mkBVar 1) $ prop, isUnsafe := false})
-  let env ← ofExceptKernelException $ env.addDecl (.axiomDecl {name := `Ne, levelParams := [`u], type := mkForall `α .implicit sortu $ ← mkArrow (mkBVar 0) $ ← mkArrow (mkBVar 1) $ prop, isUnsafe := false})
-  let env ← ofExceptKernelException $ env.addDecl (.axiomDecl {name := `True, levelParams := [], type := prop, isUnsafe := false})
-  let env ← ofExceptKernelException $ env.addDecl (.axiomDecl {name := `False, levelParams := [], type := prop, isUnsafe := false})
-  let env ← ofExceptKernelException $ env.addDecl (.axiomDecl {name := `Or, levelParams := [], type := ← mkArrow prop (← mkArrow prop prop), isUnsafe := false})
-  let env ← ofExceptKernelException $ env.addDecl (.axiomDecl {name := `And, levelParams := [], type := ← mkArrow prop (← mkArrow prop prop), isUnsafe := false})
-  let env ← ofExceptKernelException $ env.addDecl (.axiomDecl {name := `Iff, levelParams := [], type := ← mkArrow prop (← mkArrow prop prop), isUnsafe := false})
-  let env ← ofExceptKernelException $ env.addDecl (.axiomDecl {name := `Not, levelParams := [], type := ← mkArrow prop prop, isUnsafe := false})
-  let env ← ofExceptKernelException $ env.addDecl (.axiomDecl {name := `Exists, levelParams := [`u], type := mkForall `α .implicit sortu $ ← mkArrow (← mkArrow (mkBVar 0) prop) prop, isUnsafe := false})
-  let env ← ofExceptKernelException $ env.addDecl (.axiomDecl {name := `Duper.Skolem.some, levelParams := [`u], type := mkForall `α .implicit sortu $ ← mkArrow (← mkArrow (mkBVar 0) prop) $ ← mkArrow (mkBVar 1) (mkBVar 2), isUnsafe := false})
-  let env ← ofExceptKernelException $ env.addDecl (.axiomDecl {name := `Nonempty, levelParams := [`u], type := mkForall `α .default sortu prop, isUnsafe := false})
-  let env ← ofExceptKernelException $ env.addDecl (.axiomDecl
+  let env ← ofExceptKernelException $ env.addDecl opts (.axiomDecl {name := `Nat, levelParams := [], type := type, isUnsafe := false})
+  let env ← ofExceptKernelException $ env.addDecl opts (.axiomDecl {name := `Iota, levelParams := [], type := type, isUnsafe := false})
+  let env ← ofExceptKernelException $ env.addDecl opts (.axiomDecl {name := `Bool, levelParams := [], type := type, isUnsafe := false})
+  let env ← ofExceptKernelException $ env.addDecl opts (.axiomDecl {name := `Bool.false, levelParams := [], type := mkConst `Bool, isUnsafe := false})
+  let env ← ofExceptKernelException $ env.addDecl opts (.axiomDecl {name := `sorryAx, levelParams := [`u], type := mkForall `α .default sortu $ mkForall `synthetic .default (mkConst `Bool) $ mkBVar 1, isUnsafe := false})
+  let env ← ofExceptKernelException $ env.addDecl opts (.axiomDecl {name := `Eq, levelParams := [`u], type := mkForall `α .implicit sortu $ ← mkArrow (mkBVar 0) $ ← mkArrow (mkBVar 1) $ prop, isUnsafe := false})
+  let env ← ofExceptKernelException $ env.addDecl opts (.axiomDecl {name := `Ne, levelParams := [`u], type := mkForall `α .implicit sortu $ ← mkArrow (mkBVar 0) $ ← mkArrow (mkBVar 1) $ prop, isUnsafe := false})
+  let env ← ofExceptKernelException $ env.addDecl opts (.axiomDecl {name := `True, levelParams := [], type := prop, isUnsafe := false})
+  let env ← ofExceptKernelException $ env.addDecl opts (.axiomDecl {name := `False, levelParams := [], type := prop, isUnsafe := false})
+  let env ← ofExceptKernelException $ env.addDecl opts (.axiomDecl {name := `Or, levelParams := [], type := ← mkArrow prop (← mkArrow prop prop), isUnsafe := false})
+  let env ← ofExceptKernelException $ env.addDecl opts (.axiomDecl {name := `And, levelParams := [], type := ← mkArrow prop (← mkArrow prop prop), isUnsafe := false})
+  let env ← ofExceptKernelException $ env.addDecl opts (.axiomDecl {name := `Iff, levelParams := [], type := ← mkArrow prop (← mkArrow prop prop), isUnsafe := false})
+  let env ← ofExceptKernelException $ env.addDecl opts (.axiomDecl {name := `Not, levelParams := [], type := ← mkArrow prop prop, isUnsafe := false})
+  let env ← ofExceptKernelException $ env.addDecl opts (.axiomDecl {name := `Exists, levelParams := [`u], type := mkForall `α .implicit sortu $ ← mkArrow (← mkArrow (mkBVar 0) prop) prop, isUnsafe := false})
+  let env ← ofExceptKernelException $ env.addDecl opts (.axiomDecl {name := `Duper.Skolem.some, levelParams := [`u], type := mkForall `α .implicit sortu $ ← mkArrow (← mkArrow (mkBVar 0) prop) $ ← mkArrow (mkBVar 1) (mkBVar 2), isUnsafe := false})
+  let env ← ofExceptKernelException $ env.addDecl opts (.axiomDecl {name := `Nonempty, levelParams := [`u], type := mkForall `α .default sortu prop, isUnsafe := false})
+  let env ← ofExceptKernelException $ env.addDecl opts (.axiomDecl
     { name := `Eq.ndrec, levelParams := [`u1, `u2],
       type :=
         mkForall `α .implicit sortu2 $
@@ -68,14 +69,14 @@ def run (path : String) (github : Bool) : MetaM Unit := do
         mkForall `h .default (mkApp3 (mkConst ``Eq [.param `u2]) (.bvar 4) (.bvar 3) (.bvar 0)) $
         (mkApp (.bvar 3) (.bvar 1)),
       isUnsafe := false})
-  let env ← ofExceptKernelException $ env.addDecl (.axiomDecl
+  let env ← ofExceptKernelException $ env.addDecl opts (.axiomDecl
     { name := `eq_true, levelParams := [],
       type :=
         mkForall `p .implicit prop $
         mkForall `h .default (.bvar 0) $
         (mkApp3 (mkConst ``Eq [levelOne]) prop (.bvar 1) (mkConst ``True [])),
       isUnsafe := false})
-  let env ← ofExceptKernelException $ env.addDecl (.axiomDecl
+  let env ← ofExceptKernelException $ env.addDecl opts (.axiomDecl
     { name := `of_eq_true, levelParams := [],
       type :=
         mkForall `p .implicit prop $

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -1,22 +1,22 @@
-{"version": 7,
+{"version": "1.0.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/lean-auto.git",
    "type": "git",
    "subDir": null,
-   "rev": "7e475ff3bd5aa241b783546ca9700016e7a617ff",
+   "rev": "542821345b1e8eb8e244dacafa96d677d0a55340",
    "name": "auto",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "7e475ff3bd5aa241b783546ca9700016e7a617ff",
+   "inputRev": "542821345b1e8eb8e244dacafa96d677d0a55340",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "51e6e0d24db9341fb031288c298b7e6b56102253",
+   "rev": "54bb04c3119f24fde14b9068c4b2e69db52a1450",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.8.0",
+   "inputRev": "v4.9.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "Duper",

diff --git a/lakefile.lean b/lakefile.lean
@@ -2,8 +2,8 @@ import Lake
 
 open Lake DSL
 
-require auto from git "https://github.com/leanprover-community/lean-auto.git"@"7e475ff3bd5aa241b783546ca9700016e7a617ff"
-require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.8.0"
+require auto from git "https://github.com/leanprover-community/lean-auto.git"@"542821345b1e8eb8e244dacafa96d677d0a55340"
+require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.9.0"
 
 package Duper {
   precompileModules := true

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.8.0
+leanprover/lean4:v4.9.0