rename jazzct into jasmin-ct, and jazz2tex into jasmin2tex (#838)

Co-authored-by: Vincent Laporte <Vincent.Laporte@inria.fr>

.gitlab-ci.yml

@@ -87,9 +87,9 @@ ocaml:
   artifacts:
     paths:
     - compiler/_build/
+    - compiler/jasmin2tex
     - compiler/jasminc
-    - compiler/jazz2tex
-    - compiler/jazzct
+    - compiler/jasmin-ct
 
 eclib:
   stage: prove
@@ -126,7 +126,7 @@ opam-compiler:
     nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run
     'eval $(opam env) &&
      make -C compiler -j$NIX_BUILD_CORES &&
-     (cd compiler && mkdir -p bin && cp _build/default/entry/jasminc.exe bin/jasminc && cp _build/default/entry/jazz2tex.exe bin/jazz2tex && cp _build/default/entry/jazzct.exe bin/jazzct && mkdir -p lib/jasmin/easycrypt && cp ../eclib/*.ec lib/jasmin/easycrypt/)'
+     (cd compiler && mkdir -p bin && cp -L _build/install/default/bin/* bin/ && mkdir -p lib/jasmin/easycrypt && cp ../eclib/*.ec lib/jasmin/easycrypt/)'
   artifacts:
     paths:
     - compiler/bin/

CHANGELOG.md

@@ -3,6 +3,10 @@
 
 ## New features
 
+- The executable `jazzct` for checking constant time is renamed into
+  `jasmin-ct`, similarly the executable `jazz2tex` is renamed into `jasmin2tex`
+  ([PR #838](https://github.com/jasmin-lang/jasmin/pull/838)).
+
 - The instructions of the VAES extension are available through a size suffix
   (e.g., `VAESENC_256`)
   ([PR #831](https://github.com/jasmin-lang/jasmin/pull/831),
@@ -50,7 +54,7 @@
   We now support operators SLH operators as in [Typing High-Speed Cryptography
   against Spectre v1](https://ia.cr/2022/1270).
   The compilation of these is proven to preserve functional semantics.
-  We also provide a speculative CCT checker, via the `jazzct` flag `--sct`.
+  We also provide a speculative CCT checker, via the `jasmin-ct` flag `--sct`.
   ([PR #447](https://github.com/jasmin-lang/jasmin/pull/447),
    [PR #723](https://github.com/jasmin-lang/jasmin/pull/723),
    [PR #814](https://github.com/jasmin-lang/jasmin/pull/814))

compiler/.gitignore

@@ -7,5 +7,5 @@ lib*.a
 report.log
 /jasmin.mlpack
 /jasminc
-/jazz2tex
-/jazzct
+/jasmin2tex
+/jasmin-ct

compiler/Makefile

@@ -42,11 +42,9 @@ all: build
 build: native
 
 define do-build
-	$(RM) jasminc jazz2tex jazzct
-	dune build @check entry/jasminc.$(1) entry/jazz2tex.$(1) entry/jazzct.$(1)
-	ln -sf "_build/default/entry/jasminc.$(1)" jasminc
-	ln -sf "_build/default/entry/jazz2tex.$(1)" jazz2tex
-	ln -sf "_build/default/entry/jazzct.$(1)" jazzct
+	$(RM) jasminc jasmin2tex jasmin-ct
+	dune build @check @install
+	for p in _build/install/default/bin/*; do ln -sf $$p $$(basename $$p); done
 endef
 
 byte:
@@ -69,18 +67,18 @@ check-ci:
 
 clean:
 	dune clean
-	$(RM) jasminc jazz2tex jazzct
+	$(RM) jasminc jasmin2tex jasmin-ct
 
 install:
 	$(INSTALL) -m 0755 -d $(DESTDIR)$(BINDIR)
 	$(INSTALL) -m 0755 -T jasminc $(DESTDIR)$(BINDIR)/jasminc
-	$(INSTALL) -m 0755 -T jazz2tex $(DESTDIR)$(BINDIR)/jazz2tex
-	$(INSTALL) -m 0755 -T jazzct $(DESTDIR)$(BINDIR)/jazzct
+	$(INSTALL) -m 0755 -T jasmin2tex $(DESTDIR)$(BINDIR)/jasmin2tex
+	$(INSTALL) -m 0755 -T jasmin-ct $(DESTDIR)$(BINDIR)/jasmin-ct
 
 uninstall:
 	$(RM) $(DESTDIR)$(BINDIR)/jasminc
-	$(RM) $(DESTDIR)$(BINDIR)/jazz2tex
-	$(RM) $(DESTDIR)$(BINDIR)/jazzct
+	$(RM) $(DESTDIR)$(BINDIR)/jasmin2tex
+	$(RM) $(DESTDIR)$(BINDIR)/jasmin-ct
 
 # --------------------------------------------------------------------
 dist: $(DISTDIR).tgz

compiler/default.nix

@@ -9,9 +9,9 @@ stdenv.mkDerivation {
 
   installPhase = ''
     mkdir -p $out/bin
-    for p in jasminc jazz2tex jazzct
+    for p in jasminc jasmin2tex jasmin-ct
     do
-      cp _build/default/entry/$p.exe $out/bin/$p
+      cp -L _build/install/default/bin/$p $out/bin/$p
     done
   '';
 }

compiler/dune

@@ -16,17 +16,17 @@
  (libraries jasminc))
 
 (executable
- (public_name jazz2tex)
- (name jazz2tex)
- (modules jazz2tex)
+ (public_name jasmin2tex)
+ (name jasmin2tex)
+ (modules jasmin2tex)
  (flags (:standard -rectypes))
  (modes byte exe)
  (libraries commonCLI))
 
 (executable
- (public_name jazzct)
- (name jazzct)
- (modules jazzct)
+ (public_name jasmin-ct)
+ (name jasmin_ct)
+ (modules jasmin_ct)
  (flags (:standard -rectypes))
  (modes byte exe)
  (libraries commonCLI))

compiler/entry/jazz2tex.ml → compiler/entry/jasmin2tex.ml

@@ -36,7 +36,7 @@ let () =
     ]
   in
   let info =
-    Cmd.info "jazz2tex" ~version:Glob_options.version_string ~doc ~man
+    Cmd.info "jasmin2tex" ~version:Glob_options.version_string ~doc ~man
   in
   Cmd.v info Term.(const parse_and_print $ arch $ call_conv $ output $ file)
   |> Cmd.eval |> exit

compiler/entry/jazzct.ml → compiler/entry/jasmin_ct.ml

@@ -114,7 +114,7 @@ let () =
       `I ("JASMINPATH", "To resolve $(i,require) directives");
     ]
   in
-  let info = Cmd.info "jazzct" ~version:Glob_options.version_string ~doc ~man in
+  let info = Cmd.info "jasmin-ct" ~version:Glob_options.version_string ~doc ~man in
   Cmd.v info
     Term.(
       const parse_and_check $ arch $ call_conv $ infer $ slice $ speculative

compiler/jasmin.opam

@@ -13,9 +13,9 @@ build: [
 ]
 install: [
   mkdir -p "%{prefix}%/bin"
-  cp "_build/default/entry/jasminc.exe" "%{prefix}%/bin/jasminc"
-  cp "_build/default/entry/jazz2tex.exe" "%{prefix}%/bin/jazz2tex"
-  cp "_build/default/entry/jazzct.exe" "%{prefix}%/bin/jazzct"
+  cp -L "_build/install/default/bin/jasminc" "%{prefix}%/bin/jasminc"
+  cp -L "_build/install/default/bin/jasmin2tex" "%{prefix}%/bin/jasmin2tex"
+  cp -L "_build/install/default/bin/jasmin-ct" "%{prefix}%/bin/jasmin-ct"
   mkdir -p "%{prefix}%/lib/jasmin/easycrypt"
   sh -c "cp ../eclib/*.ec \"%{prefix}%/lib/jasmin/easycrypt/\""
 ]

compiler/scripts/check-cct

@@ -2,4 +2,4 @@
 
 set -ex
 
-exec $(dirname $0)/../jazzct "$@"
+exec $(dirname $0)/../jasmin-ct "$@"

compiler/src/CLI_errors.ml

@@ -60,6 +60,6 @@ let check_options () =
 
   if !latexfile <> ""
   then warning Deprecated Location.i_dummy
-         "the [-latex] option has been deprecated since March 2023; use [jazz2tex] instead";
+         "the [-latex] option has been deprecated since March 2023; use [jasmin2tex] instead";
 
   List.iter chk_out_file [ outfile; latexfile; ecfile ]