Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Port src/command.ml4 to coqpp #7

Open
XVilka opened this issue Oct 18, 2019 · 0 comments
Open

Port src/command.ml4 to coqpp #7

XVilka opened this issue Oct 18, 2019 · 0 comments

Comments

@XVilka
Copy link

XVilka commented Oct 18, 2019

coq_makefile -f Make -o CoqMakefile
camlp5 macro files not supported anymore, please port src/commands.ml4 to coqpp
Usage summary:

coq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}]
  ... [any] ... [-extra[-phony] result dependencies command]
  ... [-I dir] ... [-R physicalpath logicalpath]
  ... [-Q physicalpath logicalpath] ... [VARIABLE = value]
  ...  [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file]
  [-h] [--help]

Full list of options:

[file.v]: Coq file to be compiled
[file.ml[i4]?]: Objective Caml file to be compiled
[file.ml{lib,pack}]: ocamlbuild-style file that describes a Objective Caml
  library/module
[any] : subdirectory that should be "made" and has a Makefile itself
  to do so. Very fragile and discouraged.
[-extra result dependencies command]: add target "result" with command
  "command" and dependencies "dependencies". If "result" is not
  generic (do not contains a %), "result" is built by _make all_ and
  deleted by _make clean_.
[-extra-phony result dependencies command]: add a PHONY target "result"
 with command "command" and dependencies "dependencies". Note that
 _-extra-phony foo bar ""_ is a regular way to add the target "bar" as
 as a dependencies of an already defined target "foo".
[-I dir]: look for Objective Caml dependencies in "dir"
[-R physicalpath logicalpath]: look for Coq dependencies recursively
  starting from "physicalpath". The logical path associated to the
  physical path is "logicalpath".
[-Q physicalpath logicalpath]: look for Coq dependencies starting from
  "physicalpath". The logical path associated to the physical path
  is "logicalpath".
[VARIABLE = value]: Add the variable definition "VARIABLE=value"
[-byte]: compile with byte-code version of coq
[-opt]: compile with native-code version of coq
[-arg opt]: send option "opt" to coqc
[-install opt]: where opt is "user" to force install into user directory,
  "none" to build a makefile with no install target or
  "global" to force install in $COQLIB directory
[-f file]: take the contents of file as arguments
[-o file]: output should go in file file (recommended)
	Output file outside the current directory is forbidden.
[-h]: print this usage summary
[--help]: equivalent to [-h]
make: *** [CoqMakefile] Error 1

See #6

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

No branches or pull requests

1 participant