Add option for draft (#207)

* Implement draft option.

While developing proofs and theories, can activate a draft option that will only check the current worked-on file and assume without checking any external theorem. This prevents having to verify the whole library at every run.

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

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

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
 

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
 }

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)

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

refman/quickguide.tex

@@ -283,3 +283,15 @@ \subsubsection*{Substitution}
   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}