The Coq mailing list

[frank maltman <frank.maltman AT googlemail.com>]

Hello.

There appears to be a bug or some sort of strange behaviour when extracting
modules with signatures and axioms:

--8<--

Module Type TEST.
  Parameter foo : nat.
End TEST.

Module Test.
  Axiom foo : nat.
  Extract Inlined Constant foo => "prim_foo".
End Test.

Axiom bar : nat.
Extract Inlined Constant bar => "prim_bar".

Definition x := Test.foo + bar.

--8<--

$ coqc Test.v
$ coq
< Require Test.
< Extraction Library Test.
The file Test.ml has been created by extraction.
The file Test.mli has been created by extraction.

$ cat Test.ml
open Datatypes
open Peano

module type TEST = 
 sig 
  val foo : nat
 end

module Test = 
 struct 
  
 end

(** val x : nat **)

let x =
  plus prim_foo prim_bar

Now, adding ": TEST" to the module...

--8<--

Module Type TEST.
  Parameter foo : nat.
End TEST.

Module Test : TEST.
  Axiom foo : nat.
  Extract Inlined Constant foo => "prim_foo".
End Test.

Axiom bar : nat.
Extract Inlined Constant bar => "prim_bar".

Definition x := Test.foo + bar.

--8<--

$ coqc Test.v
$ coq
< Require Test.
< Extraction Library Test.
Warning: The following axiom must be realized in the extracted code:
 Test.foo.

The file Test.ml has been created by extraction.
The file Test.mli has been created by extraction.

$ cat test.ml
open Datatypes
open Peano

module type TEST = 
 sig 
  val foo : nat
 end

module Test = 
 struct 
  (** val foo : nat **)
  
  let foo =
    failwith "AXIOM TO BE REALIZED"
 end

(** val x : nat **)

let x =
  plus Test.foo prim_bar

Note that, now, Test.foo is an unrealized axiom!