`-emacs` mode missing?

[kodyvajjha]

I followed the instructions here and installed sail via opam. However I can't find an -emacs flag which supposedly is needed by the sail emacs mode. I guess there is something basic that I am missing, could I please get some help?

Here is the entire output of sail --help:

Sail 0.17 (sail @ opam-v2.1.5)
usage: sail <options> <file1.sail> ... <fileN.sail>

  -o <prefix>                               select output filename prefix
  --dir                                     show current Sail library directory
  -i                                        start interactive interpreter
  --is <filename>                           start interactive interpreter and execute commands in script
  --iout <filename>                         print interpreter output to file
  --interact-custom                         drop to an interactive session after running Sail. Differs from -i in that it does not set up the interpreter in the interactive shell.
  --project <file>                          sail project file defining module structure
  --variable <variable=value>               assign a module variable to a value
  --all-modules                             use all modules in project file
  --list-files                              list files used in all project files
  --config <file>                           configuration file
  --abstract-types                          (experimental) allow abstract types
  --fmt                                     format input source code
  --fmt-backup <suffix>                     create backups of formated files as 'file.suffix'
  --fmt-only <file>                         format only this file
  --fmt-skip <file>                         skip formatting this file
  -D <symbol>                               define a symbol for the preprocessor, as $define does in the source code
  --no-warn                                 do not print warnings
  --all-warnings                            print all warning messages
  --strict-var                              require var expressions for variable declarations
  --plugin <file>                           load a Sail plugin
  --just-check                              terminate immediately after typechecking
  --memo-z3                                 memoize calls to z3, improving performance when typechecking repeatedly
  --no-memo-z3                              do not memoize calls to z3 (default)
  --have-feature <symbol>                   check if a feature symbol is set by default
  --no-color                                do not use terminal color codes in output
  --string-literal-type                     use a separate string_literal type for string literals
  --grouped-regstate                        group registers with same type together in generated register state record
  --non-lexical-flow                        allow non-lexical flow typing
  --no-lexp-bounds-check                    turn off bounds checking for vector assignments in l-expressions
  --auto-mono                               automatically infer how to monomorphise code
  --mono-rewrites                           turn on rewrites for combining bitvector operations
  --mono-split <filename>:<line>:<variable> manually gives a case split for monomorphisation
  --splice <filename>                       add functions from file, replacing existing definitions where necessary
  --smt-solver <solver>                     choose SMT solver. Supported solvers are z3 (default), alt-ergo, cvc4, mathsat, vampire and yices.
  --smt-linearize                           (experimental) force linearization for constraints involving exponentials
  --Oconstant-fold                          apply constant folding optimizations
  --Oaarch64-fast                           apply ARMv8.5 specific optimizations (potentially unsound in general)
  --Ofast-undefined                         turn on fast-undefined mode
  --const-prop-mutrec                       unroll function in a set of mutually recursive functions
  --ddump-initial-ast                       (debug) dump the initial ast to stdout
  --ddump-tc-ast                            (debug) dump the typechecked ast to stdout
  --dtc-verbose <verbosity>                 (debug) verbose typechecker output: 0 is silent
  --dsmt-verbose                            (debug) print SMTLIB constraints sent to SMT solver
  --dmagic-hash                             (debug) allow special character # in identifiers
  --dno-error-filenames                     (debug) do not print filenames in errors
  --dprofile                                (debug) provide basic profiling information for rewriting passes within Sail
  --ddump-rewrite-ast <prefix>              (debug) dump the ast after each rewriting step to <prefix>_<i>.lem
  --dmono-all-split-errors                  (debug) display all case split errors from monomorphisation, rather than one
  --dmono-analysis <verbosity>              (debug) dump information about monomorphisation analysis: 0 silent, 3 max
  --dmono-continue                          (debug) continue despite monomorphisation errors
  --dmono-limit                             (debug) adjust maximum size of split allowed
  --dbacktrace <length>                     (debug) length of backtrace to show when reporting unreachable code
  --infer-effects                           (deprecated) ignored for compatibility with older versions; effects are always inferred now
  --undefined-gen                           (deprecated) ignored as undefined generation is now always the same for all Sail backends
  -v                                        print version
  --version                                 print version
  --verbose <verbosity>                     produce verbose output
  --explain-all-variables                   explain all type variables in type error messages
  --explain-constraints                     explain constraints in type error messages
  --explain-verbose                         add the maximum amount of explanation to type errors
  -h                                        display this list of options. Also available as -help or --help
  -help                                     display this list of options
  --help                                    display this list of options

Options for target latex
  --latex                 invoke the Sail latex target
  --latex-prefix <prefix> set a custom prefix for generated LaTeX labels and macro commands (default sail)
  --latex-full-valspecs   print full valspecs in LaTeX output
  --latex-abbrevs         semicolon-separated list of abbreviations to fix spacing for in LaTeX output (default 'e.g.;i.e.')

Options for targets ocaml, tofrominterp, marshal
  --marshal                             OCaml-marshal out the rewritten AST to a file
  --ocaml                               invoke the Sail ocaml target
  --ocaml-nobuild                       do not build generated OCaml
  --ocaml-trace                         output an OCaml translated version of the input with tracing instrumentation, implies -ocaml
  --ocaml-build-dir <directory>         set a custom directory to build generated OCaml
  --ocaml-coverage                      build OCaml with bisect_ppx coverage reporting (requires opam packages bisect_ppx-ocamlbuild and bisect_ppx).
  --ocaml-generators <types>            produce random generators for the given types
  --tofrominterp                        output OCaml functions to translate between shallow embedding and interpreter
  --tofrominterp-lem                    output embedding translation for the Lem backend rather than the OCaml backend, implies -tofrominterp
  --tofrominterp-mwords                 output embedding translation in machine-word mode rather than bit-list mode, implies -tofrominterp
  --tofrominterp-output-dir <directory> set a custom directory to output embedding translation OCaml

Options for target lem
  --lem                        invoke the Sail lem target
  --lem-output-dir <directory> set a custom directory to output generated Lem
  --isa-output-dir <directory> set a custom directory to output generated Isabelle auxiliary theories
  --lem-lib <filename>         provide additional library to open in Lem output
  --lem-sequential             use sequential state monad for Lem output
  --lem-mwords                 use native machine word library for Lem output
  --lem-extern-type <typename> do not generate a definition for the type

Options for target coq
  --coq                         invoke the Sail coq target
  --coq-output-dir <directory>  set a custom directory to output generated Coq
  --coq-lib <filename>          provide additional library to open in Coq output
  --coq-alt-modules <filename>  provide alternative modules to open in Coq output
  --coq-alt-modules2 <filename> provide additional alternative modules to open only in main (non-_types) Coq output, and suppress default definitions of MR and M monads
  --coq-extern-type <typename>  do not generate a definition for the type
  --coq-generate-extern-types   generate only extern types rather than suppressing them
  --coq-isla <filename>         generate Coq code for decoding Isla trace values
  --coq-record-update           use coq-record-update package's syntax for record updates
  --dcoq-undef-axioms           (debug) generate axioms for functions that are declared but not defined
  --dcoq-warn-nonex             (debug) generate warnings for non-exhaustive pattern matches in the Coq backend
  --dcoq-debug-on <function>    (debug) produce debug messages for Coq output on given function

Options for target sail
  --output-sail                 print Sail code after type checking and initial rewriting
  --output-sail-dir <directory> set a directory to output pretty-printed Sail

Options for target c
  -c                            invoke the Sail c target
  --c-include <filename>        provide additional include for C output
  --c-no-main                   do not generate the main() function
  --c-no-rts                    do not include the Sail runtime
  --c-no-lib                    do not include the Sail runtime or library
  --c-prefix <prefix>           prefix generated C functions
  --c-extra-params <parameters> generate C functions with additional parameters
  --c-extra-args <arguments>    supply extra argument to every generated C function call
  --c-specialize                specialize integer arguments in C output
  --c-preserve                  make sure the provided function identifier is preserved in C output
  --c-fold-unit                 remove comma separated list of functions from C output, replacing them with unit
  --c-coverage <file>           Turn on coverage tracking and output information about all branches and functions to a file
  --c-coverage-output <file>    The generated C will output coverage at runtime to the filename provided (default sail_coverage)
  -O                            turn on optimizations for C compilation
  --Ofixed-int                  assume fixed size integers rather than GMP arbitrary precision integers
  --Ofixed-bits                 assume fixed size bitvectors rather than arbitrary precision bitvectors
  --static                      make generated C functions static

Options for target smt
  --smt                            invoke the Sail smt target
  --smt-auto                       automatically call the smt solver on generated SMT
  --smt-auto-solver <cvc4/cvc5/z3> set the solver to use for counterexample checks (default cvc5)
  --smt-ignore-overflow            ignore integer overflow in generated SMT
  --smt-propagate-vars             propgate variables through generated SMT
  --smt-int-size <n>               set a bound of n on the maximum integer bitwidth for generated SMT (default 128)
  --smt-bits-size <n>              set a bound of 2 ^ n for bitvector bitwidth in generated SMT (default 8)
  --smt-vector-size <n>            set a bound of 2 ^ n for generic vectors in generated SMT (default 5)
  --smt-include <filename>         insert additional file in SMT output

Options for target doc
  --doc                      invoke the Sail doc target
  --doc-format <format>      Output documentation in the chosen format, either latex or asciidoc (default asciidoc)
  --doc-file <file>          Document only the provided files
  --doc-embed <plain|base64> Embed all documentation contents into the documentation bundle rather than referencing it
  --doc-compact              Use compact documentation format
  --doc-bundle <file>        Name for documentation bundle file

Options for target systemverilog
  --sv                            invoke the Sail systemverilog target
  --sv-output-dir <path>          set the output directory for generated SystemVerilog files
  --sv-include <file>             add include directive to generated SystemVerilog file
  --sv-verilate <compile|run>     Invoke verilator on generated output
  --sv-lines                      output `line directives
  --sv-comb                       output an always_comb block instead of initial block
  --sv-inregs                     take register values from inputs
  --sv-outregs                    output register values
  --sv-int-size <n>               set the maximum width for unknown integers
  --sv-bits-size <n>              set the maximum width for bitvectors with unknown width
  --sv-nostrings                  don't emit any strings, instead emit units
  --sv-nopacked                   don't emit packed datastructures
  --sv-padding                    add padding on packed unions
  --sv-unreachable <functionname> Mark function as unreachable.
  --sv-nomem                      don't emit a dynamic memory implementation
  --sv-fun2wires <functionname>   Use input/output ports instead of emitting a function call
  --sv-specialize <n>             Run n specialization passes on Sail Int-kinded type variables

[Alasdair]

Oh, that hasn't existed for a while. I realised 99% of people no longer use emacs so I started switching to a editor independent LSP implementation, but I haven't had the time to get it into a polished state.

I should probably remove those commands from the .el file. Right now the emacs-mode is effectively just the basics with syntax highlighting.

[kodyvajjha]

That's good to know, thanks! Could you suggest what a good development workflow loop for writing a spec would be like? How do you incrementally test out specs that you write?

[Alasdair]

You can use sail --just-check <files> to only typecheck. sail -i <files> gives a REPL. I would use a makefile to set up utility targets to run those commands.

[kodyvajjha]

Thanks! Looking forward to the LSP. Closing this for now.