✔ Unbound value Char.chr when compiling extracted code: · Coq users

I extracted the following code, that depends on coq-simple-io and coq-json. I had successful examples of correct compilation of code that used one or the other, coq-simple-io with Coq 8.14.0,, and coq-json with 8.13. When I try to combine both, I have the following error. See the example below.

From Coq Require Import
     Lists.List
     Strings.String
     extraction.ExtrOcamlChar
     extraction.ExtrOcamlIntConv.

From JSON Require Import
    Lexer
    Printer.

From SimpleIO Require Import
     SimpleIO
     IO_Sys.
Import IO.Notations.

Open Scope string_scope.

(* begin hide *)
Set Warnings "-extraction-opaque-accessed,-extraction".
(* end hide *)

Definition read_file (filename : ocaml_string) :=
  ch <- open_in filename ;;
  ch_len <- in_channel_length ch ;;
  s <- really_input_string ch ch_len ;;
  dummy <- close_in ch ;;
  IO.ret s.

Definition process_file (s : string) :=
  let JSON := from_string s in
  match JSON with
  | inr _ => print_endline "rooo"
  | inl _ => print_endline "ddddl"
  end.

Definition f : IO unit :=
  args <- OSys.argv ;;
  data <- read_file ("test.sh") ;;
  print_endline data ;;
  process_file (from_ostring data).

Definition y0 : io_unit := IO.unsafe_run f.

Separate Extraction y0.

So basically, this example reads a file and tries to parse it as a JSON string. (the example is a subset of my case studies, I do no expect this to work of course, as a .sh file is not a JSON one).

The extraction is done using a mere coqc read_file.v and compilation with ocamlbuild -lib unix read_file.native. It derives from examples from coq-simple-io.

+ ocamlopt.opt -c -o Ascii.cmx Ascii.ml
File "Ascii.ml", line 15, characters 23-31:
15 | let shift = fun b c -> Char.chr (((Char.code c) lsl 1) land 255 + if b then 1 else 0)
                            ^^^^^^^^
Error: Unbound value Char.chr
Command exited with code 2.

Is there any resource I should review to solve this? I installed ocaml 4.12 through opam , updating a previous installation.

Li-yao (Feb 04 2022 at 15:36):

That seems to be because Char got shadowed by ext-lib. Try adding Extraction Blacklist Char. before extracting.

Stream: Coq users

Topic: ✔ Unbound value Char.chr when compiling extracted code:

Jerome Hugues (Feb 04 2022 at 14:43):

Li-yao (Feb 04 2022 at 15:36):

Jerome Hugues (Feb 04 2022 at 15:40):

Notification Bot (Feb 04 2022 at 15:40):