diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2013-11-30 11:04:10 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2013-12-20 18:57:08 +0100 |
| commit | 8ba7983f467a6e235ba88e10be90381c9429cad2 (patch) | |
| tree | 57d30e939d0e366d59809d3d335fb767cc4d5e91 /dev/ocamldebug-coq.run | |
| parent | d1824e8e6f472385d790c52792c7bf4a5adde41d (diff) | |
configure.ml: our configure script is now written in ML :-)
configure is now just a minimal wrapper around the new configure.ml.
This configure.ml is runned with the same ocaml used during
compilation, and starts with a #load "unix.cma".
For now, this new configure script is meant to be 99% compatible
with the old one. Known incompatibilities : the --foo option format
(with two --) isn't supported anymore, use -foo options instead.
Let me know if you encounter any other changes.
Internals:
- We use our own "run" command (based on Unix.create_process) to avoid
relying on some specific shell (/bin/sh or cmd.exe).
- We should have far less issues with filename quoting under windows
since we almost never rely on (cygwin) shell anymore. This remains
to be fully tested, though.
- dev/ocamldebug-coq is slightly different now, to ease its generation
Diffstat (limited to 'dev/ocamldebug-coq.run')
| -rw-r--r-- | dev/ocamldebug-coq.run | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run new file mode 100644 index 000000000..aab03f34d --- /dev/null +++ b/dev/ocamldebug-coq.run @@ -0,0 +1,34 @@ +#!/bin/sh + +# Wrapper around ocamldebug for Coq + +# This file is to be launched via the generated script ocamldebug-coq, +# which will set the env variables $OCAMLDEBUG, $CAMLP4LIB, $COQTOP +# Anyway, just in case someone tries to use this script directly, +# here are some reasonable default values + +[ -z "$OCAMLDEBUG" ] && OCAMLDEBUG=ocamldebug +[ -z "$CAMLP4LIB" ] && CAMLP4LIB=+camlp5 +[ -z "$COQTOP" -a -d "$PWD/kernel" ] && COQTOP=$PWD +[ -z "$COQTOP" -a -d "$PWD/../kernel" ] && COQTOP=`dirname $PWD` + +exec $OCAMLDEBUG \ + -I $CAMLP4LIB \ + -I $COQTOP \ + -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar \ + -I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel \ + -I $COQTOP/library -I $COQTOP/pretyping -I $COQTOP/parsing \ + -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics \ + -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config \ + -I $COQTOP/plugins/cc -I $COQTOP/plugins/dp \ + -I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \ + -I $COQTOP/plugins/firstorder -I $COQTOP/plugins/fourier \ + -I $COQTOP/plugins/funind -I $COQTOP/plugins/groebner \ + -I $COQTOP/plugins/interface -I $COQTOP/plugins/micromega \ + -I $COQTOP/plugins/omega -I $COQTOP/plugins/quote \ + -I $COQTOP/plugins/ring -I $COQTOP/plugins/romega \ + -I $COQTOP/plugins/rtauto -I $COQTOP/plugins/setoid_ring \ + -I $COQTOP/plugins/subtac -I $COQTOP/plugins/syntax \ + -I $COQTOP/plugins/xml \ + -I $COQTOP/ide \ + "$@" |