diff --git a/CHANGES.md b/CHANGES.md index 8907b3058da95a3c484ac99aac1d076a3973ace2..ae0d96443d8c117d31ee5b836e6f97010f5d1ac4 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,8 +1,11 @@ # Change List +## 2024-02-05 +The "draft()" option can now be used at the start of a file to skip checking proofs of theorem outside this file during development. + ## 2024-01-02 -The of keyword can now be used to instantiate quantified variables in facts whose right hand side is a single universaly quantified formula. This can be combined freely with instantiation of ffree schematic symbols. Manual and tests update. +The "of" keyword can now be used to instantiate quantified variables in facts whose right hand side is a single universaly quantified formula. This can be combined freely with instantiation of ffree schematic symbols. Manual and tests update. ## 2023-12-31 diff --git a/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Recursion.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Recursion.scala index 4ca6df8a3c4bfc473835d925676d2776e2324472..c30fb7ad79535b87a0827d5d730ace29c739ed1c 100644 --- a/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Recursion.scala +++ b/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Recursion.scala @@ -17,7 +17,6 @@ import Ordinals.* * for readability and faster compilation. */ object Recursion extends lisa.Main { - // var defs private val w = variable private val x = variable diff --git a/lisa-utils/src/main/scala/lisa/prooflib/Library.scala b/lisa-utils/src/main/scala/lisa/prooflib/Library.scala index 73cc6096cc8359a3ea44e9fa086cd27cee31b556..8927c413332f74a69fa0b54c41ddcc0d2d264802 100644 --- a/lisa-utils/src/main/scala/lisa/prooflib/Library.scala +++ b/lisa-utils/src/main/scala/lisa/prooflib/Library.scala @@ -30,7 +30,16 @@ abstract class Library extends lisa.prooflib.WithTheorems with lisa.prooflib.Pro var last: Option[JUSTIFICATION] = None - var _withCache: Boolean = false + // Options for files + private[prooflib] var _withCache: Boolean = false + def withCache(using file: sourcecode.File, om: OutputManager)(): Unit = + if last.nonEmpty then om.output(OutputManager.WARNING("Warning: withCache option should be used before the first definition or theorem.")) + else _withCache = true + + private[prooflib] var _draft: Option[sourcecode.File] = None + def draft(using file: sourcecode.File, om: OutputManager)(): Unit = + if last.nonEmpty then om.output(OutputManager.WARNING("Warning: draft option should be used before the first definition or theorem.")) + else _draft = Some(file) val knownDefs: scala.collection.mutable.Map[F.ConstantLabel[?], Option[JUSTIFICATION]] = scala.collection.mutable.Map.empty diff --git a/lisa-utils/src/main/scala/lisa/prooflib/OutputManager.scala b/lisa-utils/src/main/scala/lisa/prooflib/OutputManager.scala index 74bf1592e73146c042488a2c48d8c0f4934671e2..ce3f84f8b8009fe2550783477d8cad83f0f64ec0 100644 --- a/lisa-utils/src/main/scala/lisa/prooflib/OutputManager.scala +++ b/lisa-utils/src/main/scala/lisa/prooflib/OutputManager.scala @@ -47,4 +47,6 @@ object OutputManager { def YELLOW(s: String): String = Console.YELLOW + s + Console.RESET def CYAN(s: String): String = Console.CYAN + s + Console.RESET def MAGENTA(s: String): String = Console.MAGENTA + s + Console.RESET + + def WARNING(s: String): String = Console.YELLOW + "⚠ " + s + Console.RESET } diff --git a/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala b/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala index 45cab01d15b300afb2e0e438eb659db769966ad4..b6d542ce39788d19f21aef9ff31f90231b847a2e 100644 --- a/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala +++ b/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala @@ -558,7 +558,22 @@ trait WithTheorems { import lisa.utils.Serialization.* val innerJustification: theory.Theorem = - if library._withCache then + if library._draft.nonEmpty && library._draft.get.value != file + then // if the draft option is activated, and the theorem is not in the file where the draft option is given, then we replace the proof by sorry + // println("skip!") + theory.theorem(name, goal.underlying, SCProof(SC.Sorry(goal.underlying)), IndexedSeq.empty) match { + case K.Judgement.ValidJustification(just) => + just + case wrongJudgement: K.Judgement.InvalidJustification[?] => + om.lisaThrow( + LisaException.InvalidKernelJustificationComputation( + "The final proof was rejected by LISA's logical kernel. This may be due to a faulty proof computation or lack of verification by a proof tactic.", + wrongJudgement, + Some(proof) + ) + ) + } + else if library._withCache then oneThmFromFile("cache/" + name, library.theory) match { case Some(thm) => thm // try to get the theorem from file @@ -570,6 +585,10 @@ trait WithTheorems { else prove(computeProof)._1 library.last = Some(this) + + /** + * Construct the kernel theorem from the high level proof + */ private def prove(computeProof: Proof ?=> Unit): (theory.Theorem, SCProof, List[(String, theory.Justification)]) = { try { computeProof(using proof) diff --git a/refman/lisa.pdf b/refman/lisa.pdf index ab0dec1fa62604d7969a3358bec28f10bb5b1a9c..e9c6913a9f232484957e0db00e7e50c88028430b 100644 Binary files a/refman/lisa.pdf and b/refman/lisa.pdf differ diff --git a/refman/macro.tex b/refman/macro.tex index c3f2863345317398d2aaf140466c6527efbe240e..31938969ee9abf860752d65a29bce9641227ea8e 100644 --- a/refman/macro.tex +++ b/refman/macro.tex @@ -22,6 +22,7 @@ \usepackage{array} \usepackage[T1]{fontenc} \usepackage{newunicodechar} %To map unicode in listings to a different font than Fira Code +\usepackage{tabularx} \renewcommand\sfdefault{ua1} \sloppy % better (?) margin handling diff --git a/refman/quickguide.tex b/refman/quickguide.tex index 503eaa4cad1f43602d60550dff572dba933fe782..b3c683d50215e36854fd9d19ebab92c84cf41b73 100644 --- a/refman/quickguide.tex +++ b/refman/quickguide.tex @@ -283,3 +283,15 @@ If a \lstinline|subst| is a formula rather than a proven fact, then it should be thenHave(A, f(t) === t |- P(s) /\ s===t) .by Substitution.ApplyRules(subst, f(t) === t) \end{lstlisting} + + +\subsection*{File Options} +Some options can be set at the start of a file, which will affect the behaviour of Lisa. These options are intended for use at a development stage. + +\vspace{2em} +\begin{tabularx}{0.9\columnwidth}{|l|X|} + \lstinline|draft()| & Theorems outside of the current file are assumed to be true and not checked for correctness. This can speed up repetitive runs during proof drafts. + \\[4ex] + \lstinline|withCache()| & Kernel proofs will be stored in binary files when theorems are constructed. On future runs with the option enabled, theorems will be constructed from the stored low level proofs. This skips running tactics to construct or search for proofs.\\ + +\end{tabularx} \ No newline at end of file