Stream: Dune devs & users

Topic: Rule failed for a code extraction


view this post on Zulip Mukesh Tiwari (Apr 06 2024 at 17:33):

Hi all,

I am trying to migrate a project [1] on dune build system. Everything is working fine, except when I am trying to extract an OCaml code from the formalisation [2]. I basically want to extract the Schulze.v and WidestShortestPath.v files into OCaml code but it seems I am doing something wrong.

mukesh.tiwari@Mukeshs-MacBook-Pro-2 Semiring_graph_algorithm % dune build
File "./Extraction.v", line 6, characters 0-37:
Warning: The extraction is currently set to bypass opacity, the following
opaque constant bodies have been accessed
: List.Forall_rect List.nth_in_or_default List.exists_last List.destruct_list.
 [extraction-opaque-accessed,extraction,default]
File "./Extraction.v", line 10, characters 0-48:
Warning: The extraction is currently set to bypass opacity, the following
opaque constant bodies have been accessed
: List.Forall_rect List.nth_in_or_default List.exists_last List.destruct_list.
 [extraction-opaque-accessed,extraction,default]
File "extraction/dune", line 1, characters 0-116:
1 | (coq.extraction
2 |  (prelude Extraction)
3 |  (extracted_modules Schulze WidestShortestPath)
4 |  (theories Semiring Examples))
Error: Rule failed to generate the following targets:
- extraction/Schulze.ml
- extraction/Schulze.mli
- extraction/WidestShortestPath.ml
- extraction/WidestShortestPath.mli

[1] https://github.com/mukeshtiwari/Semiring_graph_algorithm/tree/main
[2] https://github.com/mukeshtiwari/Semiring_graph_algorithm/blob/main/extraction/dune

view this post on Zulip Ali Caglayan (Apr 07 2024 at 02:26):

You are setting the output directory explicitly in the file which creates the file in the wrong place. Either you should not set it explicitly or you should chose the correct path which is _build/default/extraction/schulze etc.

view this post on Zulip Ali Caglayan (Apr 07 2024 at 02:26):

The second is correct in this case but more fragile. Doing the first would be possible with two subdirectories in extraction/ for each library you want to extract.

view this post on Zulip Mukesh Tiwari (Apr 07 2024 at 07:57):

Thanks @Ali Caglayan! I changed the extraction directory in Extraction.v to _build/default/extraction/schulze but it did not change anything; I am getting the same error.

mukesh.tiwari@Mukeshs-MacBook-Pro-2 Semiring_graph_algorithm % git diff extraction/Extraction.v
diff --git a/extraction/Extraction.v b/extraction/Extraction.v
index 3c83b5e..a383916 100644
--- a/extraction/Extraction.v
+++ b/extraction/Extraction.v
@@ -2,9 +2,9 @@
 From Coq Require Import Extraction.
 From Examples Require Import Schulze WidestShortestPath.

-Set Extraction Output Directory "_build/schulze".
+Set Extraction Output Directory "_build/default/extraction/schulze".
 Recursive Extraction Library Schulze.


-Set Extraction Output Directory "_build/widestpathcode".
+Set Extraction Output Directory "_build/default/extraction/widestpathcode".
 Recursive Extraction Library WidestShortestPath.
mukesh.tiwari@Mukeshs-MacBook-Pro-2 Semiring_graph_algorithm % dune build
File "extraction/dune", line 1, characters 0-116:
1 | (coq.extraction
2 |  (prelude Extraction)
3 |  (extracted_modules Schulze WidestShortestPath)
4 |  (theories Semiring Examples))
Error: Rule failed to generate the following targets:
- extraction/Schulze.ml
- extraction/Schulze.mli
- extraction/WidestShortestPath.ml
- extraction/WidestShortestPath.mli

view this post on Zulip Mukesh Tiwari (Apr 07 2024 at 08:13):

Some more update: it is generating the OCaml code but I don't understand the reason for the error. I am slightly puzzled by the behaviour because the instructions in Extraction.v file is about extracting in _build/default/extraction/schulze but it extracts in _build/default/extraction/_build/default/extraction/schulze with an error message.

mukesh.tiwari@Mukeshs-MacBook-Pro-2 extraction % pwd
/Users/mukesh.tiwari/Mukesh/Github/Semiring_graph_algorithm/_build/default/extraction/_build/default/extraction
mukesh.tiwari@Mukeshs-MacBook-Pro-2 extraction % ls
schulze     widestpathcode
mukesh.tiwari@Mukeshs-MacBook-Pro-2 extraction % cd schulze
mukesh.tiwari@Mukeshs-MacBook-Pro-2 schulze % ls
BinNums.ml  Datatypes.mli   Definitions.ml  Hexadecimal.mli Listprop.ml Logic.mli   Nat.ml      Number.mli  Schulze.ml  Specif.mli
BinNums.mli Decimal.ml  Definitions.mli List.ml     Listprop.mli    Mat.ml      Nat.mli     Path.ml     Schulze.mli
Datatypes.ml    Decimal.mli Hexadecimal.ml  List.mli    Logic.ml    Mat.mli     Number.ml   Path.mli    Specif.ml
mukesh.tiwari@Mukeshs-MacBook-Pro-2 schulze %

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2024 at 10:38):

@Mukesh Tiwari dune will call Coq already from the extraction dir, so you can drop the _build/... prefix.

As of today not sure we do support extracting into subdirs properly, tho that's not a big issue in the sense you don't polute your sources dir anymore. But support for this would be welcome if someone would like to hack it.

view this post on Zulip Mukesh Tiwari (Apr 07 2024 at 12:57):

Thanks @Emilio Jesús Gallego Arias ! I managed to figure that out (see the extraction file code below) and now I am getting an OCaml code into _build/extraction/schulze and _build/extractions/widestpathcode. I just don't understand the reason for the error? Does it has anything to do with rule stanza (https://dune.readthedocs.io/en/stable/reference/dune/rule.html#rule)?

From Coq Require Import Extraction.
From Examples Require Import Schulze WidestShortestPath.

Set Extraction Output Directory "./schulze".
Recursive Extraction Library Schulze.


Set Extraction Output Directory "./widestpathcode".
Recursive Extraction Library WidestShortestPath.


mukesh.tiwari@Mukeshs-MacBook-Pro-2 Semiring_graph_algorithm % dune build
File "extraction/dune", line 1, characters 0-116:
1 | (coq.extraction
2 |  (prelude Extraction)
3 |  (extracted_modules Schulze WidestShortestPath)
4 |  (theories Semiring Examples))
Error: Rule failed to generate the following targets:
- extraction/Schulze.ml
- extraction/Schulze.mli
- extraction/WidestShortestPath.ml
- extraction/WidestShortestPath.mli

Btw, the extraction code below crashes the Coq (leaving the extraction directory empty).

From Coq Require Import Extraction.
From Examples Require Import Schulze WidestShortestPath.

Set Extraction Output Directory "".
Recursive Extraction Library Schulze.


Set Extraction Output Directory "./widestpathcode".
Recursive Extraction Library WidestShortestPath.

mukesh.tiwari@Mukeshs-MacBook-Pro-2 Semiring_graph_algorithm % dune build
File "./Extraction.v", line 6, characters 0-37:
Warning: The extraction is currently set to bypass opacity, the following
opaque constant bodies have been accessed
: List.Forall_rect List.nth_in_or_default List.exists_last List.destruct_list.
 [extraction-opaque-accessed,extraction,default]
File "./Extraction.v", line 6, characters 0-37:
Error:
Anomaly "Uncaught exception Unix.Unix_error(Unix.ENOENT, "mkdir", "")."
Please report at http://coq.inria.fr/bugs/.

view this post on Zulip Ali Caglayan (Apr 07 2024 at 12:58):

That's a Coq bug that should be reported. I think you need to set the directory to "." rather than "".

view this post on Zulip Ali Caglayan (Apr 07 2024 at 12:59):

Coq doesn't handle the empty string there gracefully, but it is invalid anyway here.

view this post on Zulip Ali Caglayan (Apr 07 2024 at 13:00):

I think in your case you wanted ./shulze anyway and not ..

view this post on Zulip Mukesh Tiwari (Apr 07 2024 at 13:20):

Ali Caglayan said:

I think in your case you wanted ./shulze anyway and not ..

Yeah, I did Set Extraction Output Directory "./schulze".. The empty string was a mistake.

view this post on Zulip Ali Caglayan (Apr 07 2024 at 13:35):

OK I'm not totally sure whats going on here. Set Extraction Directory is a new feature and dune hasn't had time to adapt to it yet. I would suggest avoiding it and having two seperate extraction .v files in the schulze and widestpathcode directories and an extraction stanza in each of those. You don't have to use yet another dune file as you can add the stanza to the current dune file using the subdir stanza. https://dune.readthedocs.io/en/stable/reference/dune/subdir.html

view this post on Zulip Ali Caglayan (Apr 07 2024 at 13:36):

so you dune file should look like

(subdir schulze
 (coq.extraction
 ...))

(subdir widestshortestpath
 (coq.extraction
  ...))

view this post on Zulip Ali Caglayan (Apr 07 2024 at 13:36):

obviously with the correct directory names.

view this post on Zulip Mukesh Tiwari (Apr 07 2024 at 13:49):

Awesome! Thanks Ali! It worked. Now I just need to figure out how to call the existing OCaml code from a main.ml file and run it using Dune :)

view this post on Zulip Ali Caglayan (Apr 07 2024 at 13:51):

Since extraction only produces .ml files, you will need to attach a regular OCaml library stanza to collect them all into a usable library. You can either create a library for each extraction or experiment with (include_subdirs qualified) which will stick subdirs in a module in your OCaml library. That way main.ml can directly refer to Schulze.Foo as an extracted module. Obviously all depending on your specific use case.

view this post on Zulip Mukesh Tiwari (Apr 07 2024 at 15:52):

Now there is Dune crash. This time I added (include_subdirs qualified) in the dune file in the extraction directory (it was not certainly very wise of me but nonetheless, it crashed the dune :))

mukesh.tiwari@Mukeshs-MacBook-Pro-2 Semiring_graph_algorithm % dune build
Internal error, please report upstream including the contents of _build/log.
Description:
  ("Map.find_exn: failed to find key",
  { key =
      { pos_fname = "extraction/dune"
      ; start = { pos_lnum = 3; pos_bol = 44; pos_cnum = 45 }
      ; stop = { pos_lnum = 6; pos_bol = 114; pos_cnum = 145 }
      }
  ; keys = []
  })
Raised at Stdune__Code_error.raise in file
  "otherlibs/stdune/src/code_error.ml", line 10, characters 30-62
Called from Fiber__Core.O.(>>|).(fun) in file "vendor/fiber/src/core.ml",
  line 253, characters 36-41
Called from Fiber__Scheduler.exec in file "vendor/fiber/src/scheduler.ml",
  line 76, characters 8-11
-> required by ("<unnamed>", ())
-> required by ("load-dir", In_build_dir "default/extraction")
-> required by ("<unnamed>", ())
-> required by
   ("build-alias", { dir = In_build_dir "default"; name = "default" })
-> required by ("toplevel", ())

I must not crash.  Uncertainty is the mind-killer. Exceptions are the
little-death that brings total obliteration.  I will fully express my cases.
Execution will pass over me and through me.  And when it has gone past, I
will unwind the stack along its path.  Where the cases are handled there will
be nothing.  Only I will remain.
Internal error, please report upstream including the contents of _build/log.
Description:
  ("Map.find_exn: failed to find key",
  { key =
      { pos_fname = "extraction/dune"
      ; start = { pos_lnum = 9; pos_bol = 175; pos_cnum = 176 }
      ; stop = { pos_lnum = 12; pos_bol = 256; pos_cnum = 287 }
      }
  ; keys = []
  })
Raised at Stdune__Code_error.raise in file
  "otherlibs/stdune/src/code_error.ml", line 10, characters 30-62
Called from Fiber__Core.O.(>>|).(fun) in file "vendor/fiber/src/core.ml",
  line 253, characters 36-41
Called from Fiber__Scheduler.exec in file "vendor/fiber/src/scheduler.ml",
  line 76, characters 8-11
-> required by ("<unnamed>", ())
-> required by ("load-dir", In_build_dir "default/extraction")
-> required by ("<unnamed>", ())
-> required by
   ("build-alias", { dir = In_build_dir "default"; name = "default" })
-> required by ("toplevel", ())

view this post on Zulip Mukesh Tiwari (Apr 07 2024 at 17:44):

I have one more question, Ali. I am looking for a nice workflow for executing OCaml code, extracted from Coq, using Dune. I want to call schulze [1], inside Schulze.ml which resides insides _build/default/extraction/schulze/ directory, from main.ml file. I am not sure where should I put this main.ml file so that anyone can run the code without much of efforts.

My current plan is to create a directory Executable inside my project's home directory and copy all the extracted code, from _build/default/extraction/schulze/, into Executable/lib, put main.ml in Executable/bin, and write the dune files manually to execute the OCaml code. But I feel this is not a nice way because if I change anything in my Coq file, I need to copy the extracted code again back to Executable/lib directory (I can write a script, but I am wondering if there is a better way).

[1] https://gist.github.com/mukeshtiwari/7f31dee9a6bdab3626648d898861563f#file-schulze-ml-L103

view this post on Zulip Ali Caglayan (Apr 07 2024 at 17:45):

OK then I would avoid using include subdirectories qualified. It's a bit new and has some problems. You will have to create a library for each extracted library instead which shouldn't be a big deal.

view this post on Zulip Ali Caglayan (Apr 07 2024 at 17:45):

I would keep the extracted codes in their own libraries and have your main.ml in it's own library depending on those libraries.

view this post on Zulip Ali Caglayan (Apr 07 2024 at 17:46):

You can put main.ml anywhere you like it doesn't have to be in the extraction directory you have.

view this post on Zulip Ali Caglayan (Apr 07 2024 at 17:47):

So in each of the subdir stanzas I menitoned before you include a (library ...) stanza setup the usual way you can find in the dune manual.

view this post on Zulip Ali Caglayan (Apr 07 2024 at 17:47):

Then whatever those libraries are called, you can add them as dependencies to your main.ml library.

view this post on Zulip Mukesh Tiwari (Apr 07 2024 at 17:49):

So if I create a directory Executable and put the main.ml file and a dune file. I am assuming this dune file will be able to pick all the libraries from _build/default/extraction/schulze/? Thanks again! I am going to try and will get back to you if I have any more questions.

view this post on Zulip Mukesh Tiwari (Apr 08 2024 at 09:28):

@Ali Caglayan I have created an executable directory (https://github.com/mukeshtiwari/Semiring_graph_algorithm/tree/main/executable) with two subdirectories schulzecode and widestpathcode inside it. I have added the respective dune files in these subdirectories

(executable
 (name main)
 (libraries BinNums Datatypes Mat Nat Path))

and the corresponding main file that will --eventually-- call the OCaml code extracted from Coq

open BinNums Datatypes Mat Nat Path

let _ = print_endline "Hello, world!"

But when I am running dune build, I am getting

mukesh.tiwari@Mukeshs-MacBook-Pro-2 Semiring_graph_algorithm % dune build
File "executable/schulzecode/dune", line 3, characters 38-42:
3 |  (libraries BinNums Datatypes Mat Nat Path))
                                          ^^^^
Error: Library "Path" not found.
-> required by _build/default/executable/schulzecode/main.exe
-> required by alias executable/schulzecode/all
-> required by alias default
File "executable/widestpathcode/dune", line 3, characters 38-42:
3 |  (libraries BinNums Datatypes Mat Nat Path))
                                          ^^^^
Error: Library "Path" not found.
-> required by _build/default/executable/widestpathcode/main.exe
-> required by alias executable/widestpathcode/all
-> required by alias default

view this post on Zulip Ali Caglayan (Apr 08 2024 at 12:40):

@Mukesh Tiwari Those are not libraries. You can remove the libraries field from both of those stanzas. That's for pulling in other OCaml libraries and would be useful if main.ml was it's own executable referencing your extracted code in it's own separate library. However since you've opted to build an executable straight with the source files you don't need that.

view this post on Zulip Ali Caglayan (Apr 08 2024 at 12:40):

You might be confused with (modules) but in this case omitting it gives the default behaviour of considering all the .ml files so you don't need to worry about it.

view this post on Zulip Mukesh Tiwari (Apr 08 2024 at 17:17):

You mean my dune file should be just simply this where my main.ml file lives ?

(executable
 (name main))

I am getting this error

mukesh.tiwari@Mukeshs-MacBook-Pro-2 Semiring_graph_algorithm % dune build
File "executable/widestpathcode/main.ml", line 1, characters 13-22:
1 | open BinNums Datatypes Mat Nat Path
                 ^^^^^^^^^
Error: Syntax error
File "executable/schulzecode/main.ml", line 1, characters 13-22:
1 | open BinNums Datatypes Mat Nat Path
                 ^^^^^^^^^
Error: Syntax error
mukesh.tiwari@Mukeshs-MacBook-Pro-2 Semiring_graph_algorithm % dune build
File "executable/widestpathcode/main.ml", line 1, characters 5-12:
1 | open BinNums
         ^^^^^^^
Error: Unbound module BinNums
File "executable/schulzecode/main.ml", line 1, characters 5-12:
1 | open BinNums
         ^^^^^^^
Error: Unbound module BinNums

Do I need a dune file in this directory (https://github.com/mukeshtiwari/Semiring_graph_algorithm/tree/main/executable) as well ?

view this post on Zulip Ali Caglayan (Apr 08 2024 at 17:21):

Well the executable stanza won't be able to find the extracted .ml files. There is no library stanza attached to those.

view this post on Zulip Ali Caglayan (Apr 08 2024 at 17:22):

So think of it this way: `.v/.vo --[ coq.extraction ] --> .ml --[library]--> library stuff

view this post on Zulip Ali Caglayan (Apr 08 2024 at 17:23):

Now you want to call that library stuff whatever and then add that to the libraries field of the executable stanza you have

view this post on Zulip Ali Caglayan (Apr 08 2024 at 17:23):

So here:

(subdir schulze
 (coq.extraction
  (prelude Extraction)
  (extracted_modules Schulze)
  (theories Semiring Examples)))

(subdir widestshortestpath
 (coq.extraction
  (prelude Extraction)
  (extracted_modules WidestShortestPath)
  (theories Semiring Examples)))

I would put a library stanza after both coq.extractions in the sbudir stanza.

view this post on Zulip Ali Caglayan (Apr 08 2024 at 17:24):

Call the first schulze and the second widestshortestpath if you like

view this post on Zulip Ali Caglayan (Apr 08 2024 at 17:24):

Then in your main.ml executable stanza you write (libraries schulze widestshortestpath) that way all the moduels from your extracted libraries are now available.

view this post on Zulip Ali Caglayan (Apr 08 2024 at 17:24):

Does that make sense?

view this post on Zulip Mukesh Tiwari (Apr 08 2024 at 17:27):

Ali Caglayan said:

Does that make sense?

Thanks @Ali Caglayan ! Yes, it does make sense. I am going to do the changes and see how it goes.

view this post on Zulip Mukesh Tiwari (Apr 08 2024 at 18:19):

@Ali Caglayan If I understand you correctly, then I need to make sure that the extracted code is recognised as a library by dune. I tried to change the dune file as below but now dune complains that it does not understand library.

(subdir schulze
 (coq.extraction
  (library
    (name schulze))
  (prelude Extraction)
  (extracted_modules Schulze)
  (theories Semiring Examples)))

(subdir widestshortestpath
 (coq.extraction
  (library
    (name widestshortestpath))
  (prelude Extraction)
  (extracted_modules WidestShortestPath)
  (theories Semiring Examples)))


mukesh.tiwari@Mukeshs-MacBook-Pro-2 Semiring_graph_algorithm % dune build
File "extraction/dune", line 11, characters 3-10:
11 |   (library
        ^^^^^^^
Error: Unknown field library
File "extraction/dune", line 3, characters 3-10:
3 |   (library
       ^^^^^^^
Error: Unknown field library

view this post on Zulip Ali Caglayan (Apr 08 2024 at 18:20):

It shouldn't be inside coq.extraction:

(subdir ...
  (coq.extraction
   ...)
  (library
  ...))

view this post on Zulip Ali Caglayan (Apr 08 2024 at 18:21):

The subdir stanza might be confusing you a bit. If you like you can remove it and put a dune file in each subdirectory each with a coq.extraction and a library stanza. That's what this single dune file is doing.

view this post on Zulip Ali Caglayan (Apr 08 2024 at 18:21):

Also if it helps you can add comments with ; foo so that you can take notes for future tinkering

view this post on Zulip Mukesh Tiwari (Apr 08 2024 at 18:23):

Thanks Ali! I am just trying to wrap my head around this whole dune thing and hoping that I will get past all the complexities by porting my project to dune :)

view this post on Zulip Mukesh Tiwari (Apr 08 2024 at 19:10):

How can I add a Coq library into a dune file? I can see that Schulze.mli

open BinNums
open Datatypes
open Mat
open Nat
open Path

More code

Dune build gives the following error

File "extraction/schulze/Schulze.mli", line 1, characters 5-12:
1 | open BinNums
         ^^^^^^^
Error: Unbound module BinNums

I can see the BinNums.ml and BinNums.mli in _build/default/extraction/schulze and I believe BinNums is coming from Coq.NArith.BinNat so I tried to add the following (libraries Coq.NArith.BinNat) to dune file but it did not work.

(subdir schulze
 (coq.extraction
  (prelude Extraction)
  (extracted_modules Schulze)
  (theories Semiring Examples))
  (library
    (name schulze)
    (libraries Coq.NArith.BinNat)))

view this post on Zulip Ali Caglayan (Apr 08 2024 at 19:11):

That library stanza doesn't need any libraries. These are OCaml stanzas. The extraction code is all self-contained so you only need a name field.

view this post on Zulip Ali Caglayan (Apr 08 2024 at 19:12):

I think you need to do Recursive Extraction in your .v file

view this post on Zulip Ali Caglayan (Apr 08 2024 at 19:12):

Actually nevermind you've done that.

view this post on Zulip Ali Caglayan (Apr 08 2024 at 19:14):

There is no adding "a coq library" in OCaml code. Extracted Coq is just more OCaml code and you cannot load anything from Coq in your OCaml code.

view this post on Zulip Ali Caglayan (Apr 08 2024 at 19:15):

As to why the build isn't working, my guess is that you have't listed the extracted_modules correctly.

view this post on Zulip Ali Caglayan (Apr 08 2024 at 19:15):

You are expecting BinNums, Datatypes etc. to also come out then you will have to list those too.

view this post on Zulip Mukesh Tiwari (Apr 08 2024 at 19:45):

So I added all the libraries --that I can see in the extracted code-- but it seems there is something circular (or I am doing it wrong) and getting the following error

mukesh.tiwari@Mukeshs-MacBook-Pro-2 Semiring_graph_algorithm % dune build
File "extraction/widestshortestpath/Hexadecimal.mli", line 2, characters 0-12:
2 | open Decimal
    ^^^^^^^^^^^^
Error (warning 33 [unused-open]): unused open Widestshortestpath.Decimal.
File "extraction/schulze/Hexadecimal.mli", line 2, characters 0-12:
2 | open Decimal
    ^^^^^^^^^^^^
Error (warning 33 [unused-open]): unused open Schulze__.Decimal.
mukesh.tiwari@Mukeshs-MacBook-Pro-2 Semiring_graph_algorithm %

Modified Dune file

(subdir schulze
 (coq.extraction
  (prelude Extraction)
  (extracted_modules BinNums Datatypes Decimal Definitions Hexadecimal List Listprop Logic Mat Nat Number Path Specif Schulze)
  (theories Semiring Examples))
  (library
    (name schulze)))

view this post on Zulip Ali Caglayan (Apr 08 2024 at 19:46):

That seems fine, dune is strict when it comes to warnings hence why the unused open warning is an error.

view this post on Zulip Ali Caglayan (Apr 08 2024 at 19:47):

see https://dune.readthedocs.io/en/stable/faq.html#how-to-make-warnings-non-fatal

view this post on Zulip Ali Caglayan (Apr 08 2024 at 19:48):

You need to set an env stanza to make warnings non fatal. Just put that in a dune file at your project root and it shoukd work.

view this post on Zulip Ali Caglayan (Apr 08 2024 at 19:49):

You can play around with that so that the unused imports are only ignored but its fine to allow for all warnings for the time being.


Last updated: May 25 2024 at 21:01 UTC