Unable to build base

[bollu]

Hello,

I'm trying to build base following the instructions here. However, make -C base fails with:

╭─bollu@cantordust ~/work/hs-to-coq  ‹master*› 
╰─$ make -C base
make: Entering directory '/home/bollu/work/hs-to-coq/base'
make --no-print-directory -f "Makefile" pre-all
if [ "8.7.2" != "8.7.2" ]; then\
  echo "W: This Makefile was generated by Coq 8.7.2";\
  echo "W: while the current Coq version is 8.7.2";\
fi
make --no-print-directory -f "Makefile" real-all
"coqc"   -q  -Q .   GHC/DeferredFix.v 
coqc: too few arguments
Usage: coqc <options> <Coq options> file...

options are:
  -verbose  compile verbosely
  -image f  specify an alternative executable for Coq
  -opt      run the native-code version of Coq
  -byte     run the bytecode version of Coq
  -t        keep temporary files

Coq options are:
  -I dir                 look for ML files in dir
  -include dir           (idem)
  -R dir coqdir          recursively map physical dir to logical coqdir
  -Q dir coqdir          map physical dir to logical coqdir
  -top coqdir            set the toplevel name to be coqdir instead of Top
  -coqlib dir            set the coq standard library directory
  -exclude-dir f         exclude subdirectories named f for option -R

  -noinit                start without loading the Init library
  -nois                  (idem)
  -compat X.Y            provides compatibility support for Coq version X.Y

  -load-ml-object f      load ML object file f
  -load-ml-source f      load ML file f
  -load-vernac-source f  load Coq file f.v (Load f.)
  -l f                   (idem)
  -load-vernac-source-verbose f  load Coq file f.v (Load Verbose f.)
  -lv f                  (idem)
  -load-vernac-object f  load Coq object file f.vo
  -require path          load Coq library path and import it (Require Import path.)
  -compile f.v           compile Coq file f.v (implies -batch)
  -compile-verbose f.v   verbosely compile Coq file f.v (implies -batch)
  -o f.vo                use f.vo as the output file name
  -quick                 quickly compile .v files to .vio files (skip proofs)
  -schedule-vio2vo j f1..fn   run up to j instances of Coq to turn each fi.vio
                         into fi.vo
  -schedule-vio-checking j f1..fn   run up to j instances of Coq to check all
                         proofs in each fi.vio

  -where                 print Coq's standard library location and exit
  -config, --config      print Coq's configuration information and exit
  -v, --version          print Coq version and exit
  -print-version         print Coq version in easy to parse format and exit
  -list-tags             print highlight color tags known by Coq and exit

  -quiet                 unset display of extra information (implies -w "-all")
  -w (w1,..,wn)          configure display of warnings
  -color (yes|no|auto)   configure color output

  -q                     skip loading of rcfile
  -init-file f           set the rcfile to f
  -batch                 batch mode (exits just after arguments parsing)
  -boot                  boot mode (implies -q and -batch)
  -bt                    print backtraces (requires configure debug flag)
  -debug                 debug mode (implies -bt)
  -stm-debug             STM debug mode (will trace every transaction) 
  -emacs                 tells Coq it is executed under Emacs
  -noglob                do not dump globalizations
  -dump-glob f           dump globalizations in file f (to be used by coqdoc)
  -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes)
  -impredicative-set     set sort Set impredicative
  -indices-matter        levels of indices (and nonuniform parameters) contribute to the level of inductives
  -type-in-type          disable universe consistency checking
  -xml                   export XML files either to the hierarchy rooted in
                         the directory $COQ_XML_LIBRARY_ROOT (if set) or to
                         stdout (if unset)
  -time                  display the time taken by each command
  -profile-ltac          display the time taken by each (sub)tactic
  -m, --memory           display total heap size at program exit
                         (use environment variable
                          OCAML_GC_STATS="/tmp/gclog.txt"
                          for full Gc stats dump)
  -native-compiler       precompile files for the native_compute machinery
  -h, -help, --help      print this list of options
Makefile:645: recipe for target 'GHC/DeferredFix.vo' failed
make[1]: *** [GHC/DeferredFix.vo] Error 1
Makefile:318: recipe for target 'all' failed
make: *** [all] Error 2
make: Leaving directory '/home/bollu/work/hs-to-coq/base'

I turned on the verbose option, and the failing command is: "coqc" -q -Q . GHC/DeferredFix.v

From what I can tell, this is not how -Q is supposed to be used? coq --help says:

  -Q dir coqdir          map physical dir to logical coqdir

but here, just one directory (.) is being passed. What's going on? The -Q option appears to be generated from Makefile.conf, with

# Makefile.conf
COQMF_COQLIBS =  -Q . 
COQMF_COQLIBS_NOML = -Q .  

versions of assorted tools

coqc

╭─bollu@cantordust ~/work/hs-to-coq/base  ‹master*› 
╰─$ coqc --version
The Coq Proof Assistant, version 8.7.2 (April 2018)
compiled on Apr 23 2018 18:00:37 with OCaml 4.05.0

GHC

╭─bollu@cantordust ~/work/hs-to-coq/base  ‹master*› 
╰─$ ghc --version
The Glorious Glasgow Haskell Compilation System, version 8.5.20171221

stack

╭─bollu@cantordust ~/work/hs-to-coq/base  ‹master*› 
╰─$ stack --version                                                                                                                                        1 ↵
Version 1.6.1, Git revision f25811329bbc40b0c21053a8160c56f923e1201b (5435 commits) x86_64 hpack-0.20.0

Any help appreciated :)

[nomeata]

What is your operating system and default shell?

[nomeata]

The Makefile.conf should contain

COQMF_COQLIBS =  -Q . '' 
COQMF_COQLIBS_NOML = -Q . '' 

(note the second argument).

Do you have a fresh check-out? Maybe you created Makefile.conf some weeks ago with Coq 8.7.1, which was buggy?

[bollu]

Ah, no, it was not a fresh check-out. Yes, it is possible I had created the Makefile.conf with Coq 8.7.1. Thanks :)

For future reference, how do I regenerate the Makefile.conf correctly?

Also, feel free to close the issue.

[nomeata]

Delete it, and run make :-)