Macro to include executable lisa listings from a file

refman/.gitignore

@@ -6,3 +6,4 @@ lisa.fls
 lisa.log
 lisa.out
 lisa.toc
+src/.scala-build

refman/lisa.tex

@@ -21,7 +21,8 @@
 \date{}
 
 % PDF links and meta data
-\usepackage{hyperref} 
+%\usepackage{hyperref} 
+\usepackage{bookmark} 
 \makeatletter
 \hypersetup{
     colorlinks=true,

refman/macro.tex

@@ -184,3 +184,6 @@
 
 \DeclareMathOperator{\pick}{pick}
 
+\newcommand{\lisaCode}[3]{
+\lstinputlisting[language=lisa, frame=single,caption=\href{#1}{#2}, #3]{#1}
+}

refman/prooflib.tex

@@ -6,34 +6,7 @@ \chapter{Developping Mathematics with Prooflib}
 \autoref{fig:theoryFileExample} is a reminder from \autoref{chapt:quickguide} of the canonical way to write a theory file in Lisa.
 
 \begin{figure}
-\begin{lstlisting}[language=lisa, frame=single]
-object MyTheoryName extends lisa.Main {
-  val x = variable
-  val f = function[1]
-  val P = predicate[1]
-
-  val fixedPointDoubleApplication = Theorem( 
-    ∀(x, P(x) ==> P(f(x))) |- P(x) ==> P(f(f(x)))
-  ) {
-    assume(∀(x, P(x) ==> P(f(x))))
-    val step1 = have(P(x) ==> P(f(x))) by InstantiateForall
-    val step2 = have(P(f(x)) ==> P(f(f(x)))) by InstantiateForall
-    have(thesis) by Tautology.from(step1, step2)
-  } 
-
-  val emptySetIsASubset = Theorem(
-    ∅ ⊆ x
-  ) {
-    have((y ∈ ∅) ==> (y ∈ x)) by Tautology.from(
-                            emptySetAxiom of (x := y))
-    val rhs = thenHave (∀(y, (y ∈ ∅) ==> (y ∈ x))) by RightForall
-    have(thesis) by Tautology.from(
-                            subsetAxiom of (x := ∅, y := x), rhs)
-  }
-
-}
-\end{lstlisting}
-\caption{An example of a theory file in Lisa}
+\lisaCode{src/MyTheoryName.scala}{An example of a theory file in Lisa}{firstline=3}
 \label{fig:theoryFileExample}
 \end{figure}
 

refman/src/MyTheoryName.scala

@@ -0,0 +1,29 @@
+//> using scala 3.5.1
+//> using jar "../../../lisa/target/scala-3.5.1/lisa-assembly-0.7.jar"
+object MyTheoryName extends lisa.Main:
+  val x = variable
+  val y = variable
+  val f = function[1]
+  val P = predicate[1]
+
+  val fixedPointDoubleApplication = Theorem( 
+    ∀(x, P(x) ==> P(f(x))) |- P(x) ==> P(f(f(x)))
+  ) {
+    assume(∀(x, P(x) ==> P(f(x))))
+    val step1 = have(P(x) ==> P(f(x))) by InstantiateForall
+    val step2 = have(P(f(x)) ==> P(f(f(x)))) by InstantiateForall
+    have(thesis) by Tautology.from(step1, step2)
+  } 
+
+  val emptySetIsASubset = Theorem(
+    ∅ ⊆ x
+  ) {
+    have((y ∈ ∅) ==> (y ∈ x)) by Tautology.from(
+                            emptySetAxiom of (x := y))
+    val rhs = thenHave (∀(y, (y ∈ ∅) ==> (y ∈ x))) by RightForall
+    have(thesis) by Tautology.from(
+                            subsetAxiom of (x := ∅, y := x), rhs)
+  }
+
+  @main def show = println(emptySetAxiom)
+