Skip to content

Conversation

dhilst
Copy link

@dhilst dhilst commented May 28, 2022

I had to add this to get it compiled, I was getting this error

#=== ERROR while compiling coq-io-hello-world.1.2.0 ===========================#
# context     2.0.9 | linux/x86_64 | ocaml-base-compiler.4.12.1 | pinned(git+file:///home/geckos/code/coq-io-hello-world#master#5cf7dc99)
# path        ~/.opam/4.12.1/.opam-switch/build/coq-io-hello-world.1.2.0
# command     ~/.opam/opam-init/hooks/sandbox.sh build make -C extraction
# exit-code   2
# env-file    ~/.opam/log/coq-io-hello-world-209338-6aa130.env
# output-file ~/.opam/log/coq-io-hello-world-209338-6aa130.out
### output ###
# Hint: Recursive traversal of subdirectories was not enabled for this build,
# [...]
#   '_tags' or 'myocamlbuild.ml' file). If you have modules in subdirectories,
#   you should add the option "-r" or create an empty '_tags' file.
#   
#   To enable recursive traversal for some subdirectories only, you can use the
#   following '_tags' file:
#   
#       true: -traverse
#       <dir1> or <dir2>: traverse
#       
# make: *** [Makefile:2: build] Error 10
# make: Leaving directory '/home/geckos/.opam/4.12.1/.opam-switch/build/coq-io-hello-world.1.2.0/extraction'

More precisely, by building inside extraction:

➜  coq-io-hello-world git:(master) ✗ make -C extraction 
make: Entering directory '/home/geckos/code/coq-io-hello-world/extraction'
ocamlbuild main.native -use-ocamlfind -package io-system
+ ocamlfind ocamlopt -linkpkg -package io-system main.cmx -o main.native
ocamlfind: [WARNING] Package `threads': Linking problems may arise because of the missing -thread or -vmthread switch
File "_none_", line 1:
Error: No implementations provided for the following modules:
         Mutex referenced from /home/geckos/.opam/4.12.1/lib/lwt/unix/lwt_unix.cmxa(Lwt_main)
Command exited with code 2.
Hint: Recursive traversal of subdirectories was not enabled for this build,
  as the working directory does not look like an ocamlbuild project (no
  '_tags' or 'myocamlbuild.ml' file). If you have modules in subdirectories,
  you should add the option "-r" or create an empty '_tags' file.
  
  To enable recursive traversal for some subdirectories only, you can use the
  following '_tags' file:
  
      true: -traverse
      <dir1> or <dir2>: traverse
      
Compilation unsuccessful after building 5 targets (4 cached) in 00:00:00.
make: *** [Makefile:2: build] Error 10
make: Leaving directory '/home/geckos/code/coq-io-hello-world/extraction'

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant