From 5958c2ad1e69aa16d9a3b8670591b42308903ce9 Mon Sep 17 00:00:00 2001 From: Xingyu Xie Date: Thu, 9 Apr 2026 20:11:10 +0200 Subject: [PATCH 1/2] Add a LaTeX formatting style file Co-authored-by: Matthias Meijers --- README.md | 8 ++ assets/latex/eclistings.sty | 156 ++++++++++++++++++++++++++++++++++++ 2 files changed, 164 insertions(+) create mode 100644 assets/latex/eclistings.sty diff --git a/README.md b/README.md index 902d7bc3cb..9ef3d2917e 100644 --- a/README.md +++ b/README.md @@ -26,6 +26,7 @@ EasyCrypt is part of the [Formosa Crypto project](https://formosa-crypto.org/). - [Visual Studio Code](#visual-studio-code) - [Useful Resources](#useful-resources) - [Examples](#examples) + - [LaTeX Formatting](#latex-formatting) # Installation @@ -185,3 +186,10 @@ Examples of how to use EasyCrypt are in the `examples` directory. You will find basic examples at the root of this directory, as well as a more advanced example in the `MEE-CBC` sub-directory and a tutorial on how to use the complexity system in `cost` sub-directory. + +## LaTeX Formatting + +LaTeX style file is in `assets/latex` directory. The basic usages are +`\begin{eclst} ... \end{eclst}` (display mode) and +`\ecinl{proc main() = { ... }}` (inline mode). + diff --git a/assets/latex/eclistings.sty b/assets/latex/eclistings.sty new file mode 100644 index 0000000000..65abaad738 --- /dev/null +++ b/assets/latex/eclistings.sty @@ -0,0 +1,156 @@ +\NeedsTeXFormat{LaTeX2e} +\ProvidesPackage{eclistings}[2026/04/07 EasyCrypt listings] + +\RequirePackage{listings} +\RequirePackage{xcolor} +\RequirePackage{xparse} + +% EasyCrypt % +% Language +\lstdefinelanguage{easycrypt}{% + sensitive=true, % Case sensitive keywords + % Keywords: Meta/Specification language + morekeywords=[1]% + { + abbrev, abstract, as, assert, async, axiom, axiomatized, class, clone, + const, debug, declare, eager, ehoare, elif, else, end, equiv, exists, exit, + export, fail, for, forall, from, fun, glob, global, goal, hint, hoare, if, + import, in, include, inductive, instance, islossless, lemma, let, local, locate, + match, module, nosmt, notation, of, op, phoare, pragma, Pr, pred, print, proc, + proof, prover, qed, quantum, realize, remove, rename, require, res, return, + search, section, Self, subtype, then, theory, time, timeout, Top, type, + undo, var, while, why3, with + }, + % Keywords: Regular (i.e., non-closing) tactics + morekeywords=[2]% + { + algebra, alias, apply, async, auto, beta, + byequiv, byphoare, bypr, call, case, cbv, cfold, + change, clear, congr, conseq, cut, delta, dump, + ecall, elim, eta, exfalso, exlim, fel, field, fieldeq, fission, + fusion, gen, have, hoare, idtac, inline, interleave, iota, kill, left, logic, + modpath, move, outline, pose, pr_bounded, progress, rcondf, + rcondt, replace, rewrite, right, ring, ringeq, rnd, rndsem, rwnormal, + seq, sim, simplify, skip, sp, split, splitwhile, subst, + suff, swap, symmetry, transitivity, trivial, unroll, weakmem, wlog, + wp, zeta + }, + % Keywords: Closing tactics/tacticals + morekeywords=[3]% + { + abort, admit, admitted, assumption, by, check, done, + edit, exact, fix, reflexivity, smt, solve + }, + % Keywords: Tacticals + morekeywords=[4]% + { + do, expect, first, last, strict, try + }, + comment=[n]{(*}{*)}, % Multi-line, nested comments delimited by (* and *) + string=[d]{"}, % Strings delimited by " and ", non-escapable +} + +% Style (base/default) +\lstdefinestyle{easycrypt-base}{% + % Frame + captionpos=t, % Position caption at top (mirroring what's typical for algorithms) + frame=tb, % Top and bottom rules + framesep=\smallskipamount, % Small skip between frame and listing content + % Float placement + floatplacement=tbhp, + % Character printing and placement + upquote=true, % Print backtick and single quote as is + columns=[c]fixed, % Monospace characters, centered in their box + keepspaces=true, % Don't drop spaces for column alignment + tabsize=2, % Tabstops every 2 spaces + mathescape=false, % Don't allow escaping to LaTeX with $ + showstringspaces=false, % Don't print characters for spaces + % Line numbers + numbers=none, % No line numbers + % Basic style + basicstyle={\normalsize\ttfamily}, + % Style for (non-keyword) identifiers + identifierstyle={}, +} + +% Define default colors based on availability of colorblind colors +\makeatletter +\@ifpackageloaded{colorblind}{ + \lstdefinestyle{easycrypt-default}{% + style=easycrypt-base, + % Styles for different keyword classes + keywordstyle=[1]{\color{T-Q-B6}},% + keywordstyle=[2]{\color{T-Q-B1}},% + keywordstyle=[3]{\color{T-Q-B5}},% + keywordstyle=[4]{\color{T-Q-B4}},% + % Styles for comments and strings + commentstyle={\itshape\color{T-Q-B0}},% + stringstyle={\color{T-Q-B3}}, + % Style of line numbers (in case numbers is overwritten to true) + numberstyle={\small\color{T-Q-B0}}, + } +}{% + \lstdefinestyle{easycrypt-default}{% + style=easycrypt-base, + % Styles for different keyword classes + keywordstyle=[1]{\color{violet}},% + keywordstyle=[2]{\color{blue}},% + keywordstyle=[3]{\color{red}},% + keywordstyle=[4]{\color{olive}},% + % Styles for comments and strings + commentstyle={\itshape\color{gray}},% + stringstyle={\color{green}}, + % Style of line numbers (in case numbers is overwritten to true) + numberstyle={\small\color{gray}}, + } +} +\makeatother + +% Style for drafting/debugging (explicit spaces/tabs) +\lstdefinestyle{easycrypt-draft}{% + style=easycrypt-default, + showspaces=true, + showtabs=true, + showstringspaces=true, +} + +% Style without top/bottom frame rules +\lstdefinestyle{easycrypt-plain}{% + style=easycrypt-default, + frame=none, + framesep=0pt, +} + +% Environments +%% Default, non-floating environment +%% Meant to be used inside other (potentially floating) environment +%% that takes care of the caption and surrounding spacing +\lstnewenvironment{eclst}[1][]{% + \lstset{% + language=easycrypt,% + style=easycrypt-default,% + aboveskip=\smallskipamount,% Equal to framesep of style if top rule, else 0pt + belowskip=\smallskipamount,% Equal to framesep of style if bottom rule, else 0pt + abovecaptionskip=0pt,% + belowcaptionskip=0pt,% + #1% + }% +}{} + +% Inline +\NewDocumentCommand{\ecinl}{O{easycrypt-default} m O{}}{% + \lstinline[% + language=easycrypt,% + style=#1,% + breaklines,% + breakindent=0pt,% + columns=fullflexible,% + #3% + ]{#2}% +} + +\NewDocumentCommand{\ecinlfoot}{O{easycrypt-default} m O{}}{% + \ecinl[#1]{#2}[basicstyle={\footnotesize\ttfamily},#3]% +} + +\endinput \ No newline at end of file From 9cd2775f9601e04054696b811b6055ed895d16d0 Mon Sep 17 00:00:00 2001 From: Xingyu Xie Date: Thu, 9 Apr 2026 20:11:10 +0200 Subject: [PATCH 2/2] Update to the latest keywords list and remove the letter environment. --- assets/latex/eclistings.sty | 55 ++++++++++++++++++------------------- 1 file changed, 27 insertions(+), 28 deletions(-) diff --git a/assets/latex/eclistings.sty b/assets/latex/eclistings.sty index 65abaad738..044f4bfcf3 100644 --- a/assets/latex/eclistings.sty +++ b/assets/latex/eclistings.sty @@ -5,46 +5,47 @@ \RequirePackage{xcolor} \RequirePackage{xparse} -% EasyCrypt % -% Language +% EasyCrypt % Language \lstdefinelanguage{easycrypt}{% sensitive=true, % Case sensitive keywords - % Keywords: Meta/Specification language + % Keywords: Global morekeywords=[1]% { - abbrev, abstract, as, assert, async, axiom, axiomatized, class, clone, - const, debug, declare, eager, ehoare, elif, else, end, equiv, exists, exit, - export, fail, for, forall, from, fun, glob, global, goal, hint, hoare, if, - import, in, include, inductive, instance, islossless, lemma, let, local, locate, - match, module, nosmt, notation, of, op, phoare, pragma, Pr, pred, print, proc, - proof, prover, qed, quantum, realize, remove, rename, require, res, return, - search, section, Self, subtype, then, theory, time, timeout, Top, type, - undo, var, while, why3, with + Pr, Self, Top, abbrev, abort, abstract, as, axiom, axiomatized, clone, const, + declare, dump, end, exception, exit, export, from, global, goal, hint, import, + include, inductive, instance, lemma, local, locate, module, notation, of, op, + pred, print, proof, prover, qed, realize, remove, rename, require, search, + section, subtype, theory, timeout, type, why3, with + }, + % Keywords: internal, and programming language + morekeywords=[2]% + { + debug, fail, pragma, time, undo, async, ehoare, elif, else, equiv, exists, + for, forall, fun, glob, hoare, if, in, is, islossless, let, match, phoare, + proc, raise, res, return, then, var, while }, % Keywords: Regular (i.e., non-closing) tactics morekeywords=[2]% { - algebra, alias, apply, async, auto, beta, - byequiv, byphoare, bypr, call, case, cbv, cfold, - change, clear, congr, conseq, cut, delta, dump, - ecall, elim, eta, exfalso, exlim, fel, field, fieldeq, fission, - fusion, gen, have, hoare, idtac, inline, interleave, iota, kill, left, logic, - modpath, move, outline, pose, pr_bounded, progress, rcondf, - rcondt, replace, rewrite, right, ring, ringeq, rnd, rndsem, rwnormal, - seq, sim, simplify, skip, sp, split, splitwhile, subst, - suff, swap, symmetry, transitivity, trivial, unroll, weakmem, wlog, - wp, zeta + algebra, alias, apply, auto, beta, byehoare, byequiv, byphoare, bypr, byupto, + call, case, cbv, cfold, change, clear, congr, conseq, delta, eager, ecall, + elim, eta, exfalso, exlim, fel, field, fieldeq, fission, fusion, gen, have, + idassign, idtac, inline, interleave, iota, kill, left, logic, modpath, move, + outline, pose, pr_bounded, progress, rcondf, rcondt, replace, rewrite, right, + ring, ringeq, rnd, rndsem, rwnormal, seq, sim, simplify, skip, sp, split, + splitwhile, subst, suff, swap, symmetry, transitivity, trivial, unroll, + weakmem, wlog, wp, zeta }, - % Keywords: Closing tactics/tacticals + % Keywords: Closing/byclose tactics and dangerous commands morekeywords=[3]% { - abort, admit, admitted, assumption, by, check, done, - edit, exact, fix, reflexivity, smt, solve + assumption, by, check, coq, done, edit, exact, fix, reflexivity, smt, solve }, - % Keywords: Tacticals + % Keywords: Tacticals and dangerous commands morekeywords=[4]% { - do, expect, first, last, strict, try + do, expect, first, last, try, + admit, admitted }, comment=[n]{(*}{*)}, % Multi-line, nested comments delimited by (* and *) string=[d]{"}, % Strings delimited by " and ", non-escapable @@ -74,7 +75,6 @@ } % Define default colors based on availability of colorblind colors -\makeatletter \@ifpackageloaded{colorblind}{ \lstdefinestyle{easycrypt-default}{% style=easycrypt-base, @@ -104,7 +104,6 @@ numberstyle={\small\color{gray}}, } } -\makeatother % Style for drafting/debugging (explicit spaces/tabs) \lstdefinestyle{easycrypt-draft}{%