Skip to content

Commit 49f6822

Browse files
committed
fix: refined language around --precompute-only
1 parent 3b1b897 commit 49f6822

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

languages/tamarin.tex

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -311,7 +311,7 @@ \subsubsection{Other Tips and Tricks}
311311

312312
\begin{itemize}
313313

314-
\item If you run ``\texttt{tamarin-prover theory.spthy}'' on the command line, Tamarin will check the theory's syntax but not attempt to prove any lemmas. This can be useful for quick sanity checking. However, an even more useful command is ``\texttt{tamarin-prover -{}-precompute-only theory.spthy}'', which not only checks the theory's syntax but also reports the numbers of partial deconstructions both before and after source refinement. This is typically almost as fast as only doing the syntax check, but provides substantially more useful information.
314+
\item If you run ``\texttt{tamarin-prover theory.spthy}'' on the command line, Tamarin will check the theory's syntax but not attempt to prove any lemmas. This can be useful for quick sanity checking. However, an even more useful command is ``\texttt{tamarin-prover -{}-precompute-only theory.spthy}'', which not only checks the theory's syntax but also reports the numbers of partial deconstructions both before and after source refinement. This is often almost as fast as only doing the syntax check (especially for small theories), but even when it takes a significant amount of time it provides substantially more useful information.
315315

316316
\item There is an official \href{https://marketplace.visualstudio.com/items?itemName=tamarin-prover.tamarin-prover}{Visual Studio Code plugin for Tamarin}, which works very well for syntax highlighting and error detection on the Tamarin rules-based syntax; however, as of this writing (April 2025) it struggles with the SAPIC+ syntax, reporting both spurious syntax errors and spurious errors about action facts (SAPIC+ events) not being declared. We strongly recommend that Visual Studio Code users install the plugin and use it when writing rules-based theories, but do not recommend using it when writing SAPIC+ theories.
317317

0 commit comments

Comments
 (0)