Scroll to navigation

SERNAME(1) User Commands SERNAME(1)

NAME

sername - manual page for sername

DESCRIPTION

NAME

sername - sername Coq tool

SYNOPSIS

sername [OPTION]??? FILE

DESCRIPTION

Experimental Coq name serializer.

USAGE

To serialize names listed in `names.txt` in module `Funs.mod`:
sername -Q fs,Funs --require-lib=Funs.mod names.txt
See the documentation on the project's webpage for more information.

ARGUMENTS

FILE (required)
Input file.

OPTIONS

--async=COQTOP

Enable async support using Coq binary COQTOP (experimental).

--async-workers=VAL (absent=3)

Maximum number of async workers.

--body

Print bodies of constrs.

--coqlib=COQPATH (absent=/usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq)

Load Coq.Init.Prelude from COQPATH; plugins/ and theories/ should live there.

--de-bruijn

Print constrs with de Bruijn indices.

--debug

Enable debug mode for Coq.

--disallow-sprop

Forbid using the proof irrelevant SProp sort (allowed by default)

--error-recovery

Enable Coq's error recovery inside tactics and commands.

--exn_on_opaque

[debug option] raise an exception on non-serializeble terms

-I DIR, --ml-include-path=DIR

Include DIR in default loadpath, for locating ML files

--impredicative-set

Enable Coq -impredicative-set option (disabled by default)

--indices-matter

Levels of indices (and nonuniform parameters) contribute to the level of inductives (disabled by default)

--omit_att

[debug option] omit attribute nodes

--omit_env

[debug option] turn enviroments into abstract objects

--omit_loc

[debug option] shorten location printing

--printer=VAL (absent=sertop)

one of sertop, a custom printer (UTF-8 with emacs-compatible quoting), human, sexplib's human-format printer (recommended for debug sessions) or mach, sexplib's machine-format printer

-Q DIR,LP, --load-path=DIR,LP

Bind a logical loadpath LP to a directory DIR

--quick

Skip checking opaque proofs (very experimental).

-R DIR,LP, --rec-load-path=DIR,LP

Bind a logical loadpath LP to a directory DIR and implicitly open its namespace.

--require-lib=VAL

Coq module to require.

--str-pp

Pretty-print constr strings.

COMMON OPTIONS

--help[=FMT] (default=auto)

Show this help in format FMT. The value FMT must be one of auto, pager, groff or plain. With auto, the format is pager or plain whenever the TERM env var is dumb or undefined.

--version

Show version information.

EXIT STATUS

sername exits with:
0
on success.
123 on indiscriminate errors reported on standard error.
124 on command line parsing errors.
125 on unexpected internal errors (bugs).

SEE ALSO

The full documentation for sername is maintained as a Texinfo manual. If the info and sername programs are properly installed at your site, the command

info sername

should give you access to the complete manual.

August 2024 sername