6. How To Use The Cogent Compiler

6.1. Command-line Arguments

The Cogent compiler accepts a large number of command-line arguments, which are either commands, directing the compiler to produce particular outputs, or flags, influencing the compiler’s behaviour as it works.

A typical invocation might be:

$ cogent -g -o generated \
         --infer-c-funcs=main.ac \
         --infer-c-types=abstract/Grid.ah \
         mandelbrot.cogent

6.1.1. Commands

--ast-c	parse C file with Cogent antiquotation and print AST
--stack-usage=FILE
	parse a stack usage .su file generated by gcc; FILE optional
--parse	parse Cogent source code
-t, --typecheck
	typecheck surface program
-d, --desugar	desugar surface program and re-type it
--normal	normalise core language and re-type it
--simplify	simplify core language and re-type it
--mono	monomorphise core language and re-type it
-g, --code-gen	generate C code
--ast-parse	display surface language AST
--ast-tc	display type-checked surface language AST
--ast-desugar	display desugared core language AST
--ast-normal	display normalised core language AST
--ast-simpl	display simplified core language AST
--ast-mono	display monomorphised core language AST
-i, --repl	run Cogent REPL
--docgent	generate HTML documentation from Docgent comments; must be enabled at Cogent compile time
--pretty-parse	pretty-print surface language
-T, --pretty-tc
	pretty-print type-checked surface language
-D, --pretty-desugar
	pretty-print desugared core language
--pretty-normal
	pretty-print normalised core language
--pretty-simpl	pretty-print simplified core language
--pretty-mono	pretty-print monomorphised core language
--hs-shallow-desugar
	generate Haskell shallow embedding (desugared core)
--hs-shallow-desugar-tuples
	generate Haskell shallow embedding (desugared core, with Haskell tuples)
--hs-ffi	generate Haskell FFI code to access generated C code (including a .hsc module for types and a .hs module for functions)
--deep-desugar	generate Isabelle deep embedding (desugared core)
--deep-normal	generate Isabelle deep embedding (normalised core)
--deep-mono	generate Isabelle deep embedding (monomorphised core)
--shallow-desugar
	generate Isabelle shallow embedding (desugared core)
--shallow-normal
	generate Isabelle shallow embedding (normalised core)
--shallow-mono	generate Isabelle shallow embedding (monomorphised core)
--shallow-desugar-tuples
	enerate Isabelle shallow embedding (desugared core, with HOL tuples)
--scorres-desugar
	generate scorres (desugared core)
--scorres-normal
	generate scorres (normalised core)
--scorres-mono	generate scorres (monomorphised core)
--shallow-consts-desugar
	generate constant definitions for shallow embedding (desugared core)
--shallow-consts-normal
	generate constant definitions for shallow embedding (normalised core)
--shallow-consts-mono
	generate constant definitions for shallow embedding (monomorphised core)
--shallow-consts-desugar-tuples
	generate constant definitions for shallow embedding (desugared core, with HOL tuples)
--shallow-tuples-proof
	generate proof for shallow tuples embedding
--normal-proof	generate Isabelle proof of normalisation
--mono-proof	generate monomorphisation proof
--ac-install	generate an Isabelle theory to install AutoCorres
--corres-setup	generate Isabelle lemmas for c-refinement
--corres-proof	generate Isabelle proof of c-refinement
--type-proof-normal
	generate Isabelle proof of type correctness of normalised AST
--type-proof	generate Isabelle proof of type correctness of normal-mono AST
--all-refine	generate shallow-to-C refinement proof (collective)
--root	generate an Isabelle ROOT file
--table-c-types
	generate a table of Cogent and C type correspondence
--table-shallow
	generate a table of type synonyms for shallow embedding
--table-abs-func-mono
	generate a table of monomorphised abstract functions
--table-abs-type-mono
	generate a table of monomorphised abstract types
-G, --graph-gen
	generate graph for graph-refine
--build-info	log how cogent is being invoked by generating BUILD_INFO file; implied by any collective commands
-C, --c-refinement
	generate all files needed for the C refinement proof (collective)
-F, --functional-correctness
	generate all files needed for the functional correctness proof (collective)
-A, --all	generate all possible outputs (collective)
-Q, --quickcheck
	generate QuickCheck related artifacts (collective)
--libgum-dir	display directory where standard gum headers are installed (can be set by the $COGENT_LIBGUM_DIR environment variable)
-v, -V, --version
	show version number

6.1.2. All Flags

-o NAME, --output-name=NAME
	specify base name for output files; by default, derived from name of source Cogent file
--proof-name=NAME
	specify Isabelle theory file name; by default, derived from name of source Cogent file
--abs-type-dir=PATH
	abstract type definitions will be in PATH/abstract/, which must exist (default is ./)
--dist-dir=PATH
	specify path to all output files (default is ./)
--fake-header-dir=PATH
	specify path to fake C header files
-I PATH, --include=PATH
	specify directories to search for included cogent files
--root-dir=PATH
	specify path to top-level directory (for imports in theory files only, default is ./)
--arch=ARCH	set the target architecture; ARCH could be one of arm32 (default), x86_64, x86
--cust-ty-gen=FILE
	config file to customise type generation
--entry-funcs=FILE
	give a list of Cogent functions that are only called from outside
--ext-types=FILE
	give external type names to C parser
--infer-c-funcs=FILE
	infer Cogent abstract function definitions (can be specified multiple times)
--infer-c-types=FILE
	infer Cogent abstract type definitions (can be specified multiple times)
--name-cache=FILE
	specify the name cache file to use
--proof-input-c=FILE
	specify input C file to generate proofs; defaults to the same base name as input Cogent file
--prune-call-graph=FILE
	specify Cogent entry-point definitions
--cogent-pp-args=ARG
	arguments given to Cogent preprocessor (same as for cpphs; can be specified multiple times)
--cpp=PROG	set which C-preprocessor to use (default to cpp)
--cpp-args=ARG	arguments given to C-preprocessor (default to $CPPIN -P -o $CPPOUT)
--ddump-smt	dump verbose SMT-solving information
--ddump-tc	dump (massive) surface typechecking internals
--ddump-tc-ctx	dump surface typechecking with context
--ddump-tc-filter=KEYWORDS
	a space-separated list of keywords to indicate which groups of info to display; possible keywords are gen, sol, post, tc
--ddump-to-file=FILE
	dump debugging output to specific file instead of terminal
--ddump-pretty-ds-no-tc
	dump the pretty printed desugared expression before typechecking
--ddump-pretty-normal-no-tc
	dump the pretty printed normalised expression before typechecking
--fcheck-undefined, --fno-check-undefined
	check for undefined behaviours in C (default enabled)
-B, --fdisambiguate-pp
	when pretty-printing, also display internal representation as comments
--fffi-c-functions
	generate FFI functions in the C code (should be used when -Q/--quickcheck is specified)
--fflatten-nestings, --fno-flatten-nestings
	flatten out nested structs in C code (does nothing; default is disabled)
--ffncall-as-macro, --fno-fncall-as-macro
	generate macros instead of real function calls (default is disabled)
--ffull-src-path
	display full path for source file locations
--ffunc-purity-attr, --fno-func-purity-attr
	generate GCC attributes to classify purity of Cogent functions (default is enabled)
--fgen-header, --fno-gen-header
	generate build info header in all output files (default is disabled)
--fintermediate-vars, --fno-intermediate-vars
	generate intermediate variables for Cogent expressions (default is enabled)
--flax-take-put, --fno-lax-take-put
	allow take/put type operators on abstract datatypes (default is disabled)
--flet-in-if, --fno-let-in-if
	put binding of a let inside an if-clause (default is enabled)
--fletbang-in-if, --fno-letbang-in-if
	put binding of a let! inside an if-clause (default is enabled)
--fml-typing-tree, --fno-ml-typing-tree
	generate ML typing tree in type proofs (default is enabled)
--fnormalisation=NF, --fno-normalisation
	normalise (or don’t normalise) the core language to the NF normal form, which may be anf, knf, or lnf; the default is to normalise to anf
--fpragmas, --fno-pragmas
	preprocess pragmas (default is enabled)
--fpretty-errmsgs, --fno-pretty-errmsgs
	enable/disable pretty-printing of error messages (requires ANSI support; default is enabled)
--freverse-tc-errors, --fno-reverse-tc-errors
	reverse the order of type errors printed
--fshare-linear-vars, --fno-share-linear-vars
	reuse C variables for linear objects (default is disabled)
--fshow-types-in-pretty, --fno-show-types-in-pretty
	show inferred types of each AST node when doing pretty-printing (default is disabled)
--fsimplifier, --fno-simplifier
	enable or disabled simplifier on core language (default is disabled)
--fsimplifier-level=NUMBER
	number of iterations simplifier does (default is 4; no effect if simplifier disabled)
--fstatic-inline, --fno-static-inline
	mark generated C functions as static inline (default is enabled)
--ftuples-as-sugar, --fno-tuples-as-sugar
	treat tuples as syntactic sugar to unboxed records, which gives better performance; or don’t (default is enabled)
--ftc-ctx-constraints, --fno-tc-ctx-constraints
	display (or don’t display) constraints in type errors (default is disabled)
--ftc-ctx-len=NUMBER
	set the depth for printing error context in typechecker (default is 3)
--ftp-with-bodies, --fno-tp-with-bodies
	generate type proof with bodies (default is enabled)
--ftp-with-decls, --fno-typ-with-decls
	generate type proof with declarations (default is enabled)
--funion-for-variants, --fno-union-for-variants
	use union types for variants in C code; this cannot be verified (default is disabled)
--funtyped-func-enum, --fno-untyped-func-enum
	use untyped function enum type (default is enabled)
--fuse-compound-literals, --fno-use-compound-literals
	use compound literals when possible in C code; otherwise, create new variables (default is enabled)
--fwrap-put-in-let, --fno-wrap-put-in-let
	Put always appears in a Let-binding when normalised (default is disabled)
-O LEVEL, --optimisation=LEVEL
	set optimisation level to one of -O0, [TODO] no optimisations; -O1, [TODO] some optimisations; -O2, [TODO] more optimisations; -Od, [TODO] (default); -On, [TODO]; -Os, [TODO] size; -Ou, [TODO]
--Wall	issue all warnings
-w, --Wno-warn	turn off all warnings
--Wwarn	warnings are treated only as warnings, not as errors (default is enabled)
-E, --Werror	make any warning into a fatal error (default is disabled)
--Wdodgy-take-put, --Wno-dodgy-take-put
	enable/disable warnings on ill-formed take or put in types (default is enabled)
--Wdynamic-variant-promotion, --Wno-dynamic-variant-promotion
	enable/disable warnings on dynamic variant type promotion (default is disabled)
--Wimplicit-int-lit-promotion, --Wno-implicit-int-lit-promotion
	enable/disable warning on implicit integer literal promotion (default is enabled)
--Wmono, --Wno-mono
	enable/disable warnings during monomorphisation (default is disabled)
--Wunused-local-binds, --Wno-unused-local-binds
	enable/disable warnings about unused local binders (default is disabled)
-q, --quiet	do not display compilation progress
-x, --fdump-to-stdout
	dump all output to stdout
--interactive	interactive compiler mode
--type-proof-sorry-before=FUN_NAME
	bad hack: sorry all type proofs for functions that precede given function name