Configuration
We present the configuration mechanism of coq-of-ocaml
to define some global settings. We write the configuration in a file in the JSON format. To run coq-of-ocaml
with a configuration file, use the -config
option:
coq-of-ocaml -config configuration.json ...
The general structure of a configuration file is an object of entry keys and values:
{
"entry_1": value_1,
...,
"entry_n": value_n
}
An example is:
{
"error_message_blacklist": [
"Unbound module Tezos_protocol_alpha_functor"
],
"monadic_operators": [
["Error_monad.op_gtgteq", "let="],
["Error_monad.op_gtgteqquestion", "let=?"],
["Error_monad.op_gtgtquestion", "let?"]
],
"require": [
["Tezos_raw_protocol_alpha", "Tezos"]
],
"variant_constructors": [
["Dir", "Context.Dir"],
["Key", "Context.Key"],
["Hex", "MBytes.Hex"]
],
"without_positivity_checking": [
"src/proto_alpha/lib_protocol/storage_description.ml"
]
}
The configuration entries are described as follows.
alias_barrier_modules
Example
"alias_barrier_modules": [
"Tezos_protocol_environment_alpha__Environment"
]
Value
A list of module names at which to stop when iterating through record aliases to find the initial record definition.
Explanation
An example of OCaml code with a record alias is:
module A = struct
type t = {a : string; b : bool}
end
module B = struct
type t = A.t = {a : string; b : bool}
end
let x = {B.a = "hi"; b = true}
which generates:
Module A.
Module t.
Record record : Set := Build {
a : string;
b : bool }.
Definition with_a a (r : record) :=
Build a r.(b).
Definition with_b b (r : record) :=
Build r.(a) b.
End t.
Definition t := t.record.
End A.
Module B.
Definition t : Set := A.t.
End B.
Definition x : B.t := {| A.t.a := "hi"; A.t.b := true |}.
Even if in OCaml we can talk about the field B.a
, in Coq we transform it to A.t.a
so that there is a single record definition. To do this transformation, we go through the record aliases up to the alias barriers, if any.
constant_warning
Example
"constant_warning": false
Value
A boolean to select if there should be a warning in the generated code on some constants. A typical example are the integer constants which are all treated as int
. The default of this option is true
.
Explanation
Without setting this option to false
, the output of the following code:
let n : int64 = 12L
is:
Definition n : int64 :=
(* ❌ Constant of type int64 is converted to int *)
12.
Setting the constant_warning
option to false
we get:
Definition n : int64 := 12.
constructor_map
Example
"constructor_map": [
["public_key_hash", "Ed25519", "Ed25519Hash"],
["public_key_hash", "P256", "P256Hash"],
["public_key_hash", "Secp256k1", "Secp256k1Hash"]
]
Value
A list of triples with a type name, a constructor name and a new constructor name to rename to. The type name must be the type name associated to the constructor, and is not prefixed by a module name. This type name is mostly there to help to disambiguate.
Explanation
In OCaml we can have different types with the same constructor names, as long as the OCaml compiler can differentiate them based on type information. In Coq this is not the case. The definition of two constructors with the same name generates a name collision. For this reason, we can selectively rename some constructors in coq-of-ocaml
in order to avoid name collisions in Coq.
error_category_blacklist
Example
"error_category_blacklist": [
"extensible_type",
"module",
"side_effect"
]
Value
A list of error categories to black-list. The category of an error message is given in its header. For example:
--- foo.ml:1:1 ------------------------------------------- side_effect (1/1) ---
> 1 | let () =
> 2 | print_endline "hello world"
3 |
Top-level evaluations are ignored
is an error of category side_effect
.
Explanation
We may want to ignore some categories of errors in order to focus on other errors in a CI system for example.
error_filename_blacklist
Example
"error_filename_blacklist": [
"src/proto_alpha/lib_protocol/alpha_context.ml",
"src/proto_alpha/lib_protocol/alpha_context.mli"
]
Value
A list of file names on which not to fail, even in case of errors. The return code of coq-of-ocaml
is then 0 (success). We still display the error messages.