From 141a21da29216a43eb067ef0fcb9c7d914d45bdc Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 3 Apr 2009 14:51:52 +0000 Subject: Ocamlbuild: improvements suggested by N. Pouillard * Import of Coq_config via myocamlbuild_config.ml, instead of my get_env * As a consequence, we enrich this Coq_config with stuff that was only in config/Makefile * replace the big ugly find by some dependencies against source files * by the way: build csdpcert, with the right aliases. I've tried to escape things properly for windows in ./configure, but this isn't fully tested yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12046 85f007b7-540e-0410-9357-904b9bb8a0f7 --- build | 8 +- config/coq_config.mli | 15 ++ configure | 207 +++++++++++----------- coq.itarget | 3 +- myocamlbuild.ml | 146 ++++++++-------- plugins/plugins.itarget | 3 + plugins/pluginsbyte.itarget | 25 +++ plugins/pluginsopt.itarget | 25 +++ plugins/pluginsvo.itarget | 60 +++++++ theories/theories.itarget | 348 +++++++++++++++++++++++++++++++++++++ vo.itarget | 407 -------------------------------------------- 11 files changed, 667 insertions(+), 580 deletions(-) create mode 100644 plugins/plugins.itarget create mode 100644 plugins/pluginsbyte.itarget create mode 100644 plugins/pluginsopt.itarget create mode 100644 plugins/pluginsvo.itarget create mode 100644 theories/theories.itarget delete mode 100644 vo.itarget diff --git a/build b/build index 4552d5a43..26237b705 100755 --- a/build +++ b/build @@ -3,14 +3,20 @@ FLAGS= OCAMLBUILD=ocamlbuild +check_config() { + [ -f config/coq_config.ml ] || (echo "please run ./configure first"; exit 1) + [ -L myocamlbuild_config.ml ] || ln -sf config/coq_config.ml myocamlbuild_config.ml +} + ocb() { + check_config $OCAMLBUILD $FLAGS $* } rule() { case $1 in - clean) ocb -clean && rm -rf bin/*;; + clean) ocb -clean && rm -rf bin/* && rm -f myocamlbuild_config.ml;; all) ocb coq.otarget;; *) ocb $1;; esac; diff --git a/config/coq_config.mli b/config/coq_config.mli index 7c80a96d4..3598b938d 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -13,12 +13,26 @@ val local : bool (* local use (no installation) *) val coqlib : string (* where the std library is installed *) val coqsrc : string (* where are the sources *) +val ocaml : string (* names of ocaml binaries *) +val ocamlc : string +val ocamlopt : string +val ocamlmklib : string +val ocamldoc : string +val ocamldep : string +val ocamlyacc : string +val ocamllex : string + val camlbin : string (* base directory of OCaml binaries *) val camllib : string (* for Dynlink *) val camlp4 : string (* exact name of camlp4: either "camlp4" ou "camlp5" *) +val camlp4o : string (* name of the camlp4o/camlp5o executable *) val camlp4bin : string (* base directory for Camlp4/5 binaries *) val camlp4lib : string (* where is the library of Camlp4 *) +val camlp4compat : string (* compatibility argument to camlp4/5 *) + +val coqideincl : string (* arguments for building coqide (e.g. lablgtk) *) +val cflags : string (* arguments passed to gcc *) val best : string (* byte/opt *) val arch : string (* architecture *) @@ -46,3 +60,4 @@ val browser : string variable COQREMOTEBROWSER *) val has_natdynlink : bool +val natdynlinkflag : string (* special cases of natdynlink (e.g. MacOS 10.5) *) diff --git a/configure b/configure index 7b39eb422..894e43d64 100755 --- a/configure +++ b/configure @@ -875,9 +875,51 @@ echo " documentation will be copied in $DOCDIR" echo " emacs mode will be copied in $EMACSLIB" echo "" -##################################################### -# Building the $COQTOP/config/coq_config.ml file -##################################################### +################################################## +# Building the $COQTOP/dev/ocamldebug-coq file +################################################## + +OCAMLDEBUGCOQ=$COQSRC/dev/ocamldebug-coq + +if test "$coq_debug_flag" = "-g" ; then + rm -f $OCAMLDEBUGCOQ + sed -e "s|COQTOPDIRECTORY|$COQTOP|" \ + -e "s|COQLIBDIRECTORY|$LIBDIR|" \ + -e "s|CAMLBINDIRECTORY|$CAMLBIN|" \ + -e "s|CAMLP4LIBDIRECTORY|$FULLCAMLP4LIB|"\ + $OCAMLDEBUGCOQ.template > $OCAMLDEBUGCOQ + chmod a-w,a+x $OCAMLDEBUGCOQ +fi + +#################################################### +# Fixing lablgtk types (before/after 2.6.0) +#################################################### + +if [ ! "$COQIDE" = "no" ]; then + if grep "class view " "$lablgtkdir/gText.mli" | grep -q "\[>" ; then + if grep -q "?accepts_tab:bool" "$lablgtkdir/gText.mli" ; then + cp -f ide/undo_lablgtk_ge212.mli ide/undo.mli + else + cp -f ide/undo_lablgtk_ge26.mli ide/undo.mli + fi + else + cp -f ide/undo_lablgtk_lt26.mli ide/undo.mli + fi +fi + +############################################## +# Creation of configuration files +############################################## + +mlconfig_file="$COQSRC/config/coq_config.ml" +config_file="$COQSRC/config/Makefile" +config_template="$COQSRC/config/Makefile.template" + + +### Warning !! +### After this line, be careful when using variables, +### since some of them (e.g. $COQSRC) will be escaped + # An escaped version of a variable escape_var () { @@ -888,65 +930,72 @@ EOF # Escaped version of browser command export BROWSER -ESCBROWSER=`VAR=BROWSER escape_var` +BROWSER=`VAR=BROWSER escape_var` # damned backslashes under M$Windows case $ARCH in win32) - ESCCOQTOP=`echo $COQTOP |sed -e 's|\\\|\\\\\\\|g'` - ESCBINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'` - ESCSRCDIR=`cygpath -m $COQSRC |sed -e 's|\\\|\\\\\\\|g'` - ESCLIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'` - ESCCAMLDIR=`echo $CAMLBIN |sed -e 's|\\\|\\\\\\\|g'` - ESCCAMLLIB=`echo $CAMLLIB |sed -e 's|\\\|\\\\\\\|g'` - ESCMANDIR=`echo $MANDIR |sed -e 's|\\\|\\\\\\\|g'` - ESCDOCDIR=`echo $DOCDIR |sed -e 's|\\\|\\\\\\\|g'` - ESCEMACSLIB=`echo $EMACSLIB |sed -e 's|\\\|\\\\\\\|g'` - ESCCOQDOCDIR=`echo $COQDOCDIR |sed -e 's|\\\|\\\\\\\|g'` - ESCCAMLP4BIN=`echo $CAMLP4BIN |sed -e 's|\\\|\\\\\\\|g'` - ESCCAMLP4LIB=`echo $CAMLP4LIB |sed -e 's|\\\|\\\\\\\|g'` - ESCLABLGTKINCLUDES=`echo $LABLGTKINCLUDES |sed -e 's|\\\|\\\\\\\|g'` - ESCCOQRUNBYTEFLAGS=`echo $COQRUNBYTEFLAGS |sed -e 's|\\\|\\\\\\\|g'` - ESCCOQTOOLSBYTEFLAGS=`echo $COQTOOLSBYTEFLAGS |sed -e 's|\\\|\\\\\\\|g'` - ESCBUILDLDPATH=`echo $BUILDLDPATH |sed -e 's|\\\|\\\\\\\|g'` -;; - *) - ESCCOQTOP="$COQTOP" - ESCBINDIR="$BINDIR" - ESCSRCDIR="$COQSRC" - ESCLIBDIR="$LIBDIR" - ESCCAMLDIR="$CAMLBIN" - ESCCAMLLIB="$CAMLLIB" - ESCMANDIR="$MANDIR" - ESCDOCDIR="$DOCDIR" - ESCEMACSLIB="$EMACSLIB" - ESCCOQDOCDIR="$COQDOCDIR" - ESCCAMLP4BIN="$CAMLP4BIN" - ESCCAMLP4LIB="$CAMLP4LIB" - ESCLABLGTKINCLUDES="$LABLGTKINCLUDES" - ESCCOQRUNBYTEFLAGS="$COQRUNBYTEFLAGS" - ESCCOQTOOLSBYTEFLAGS="$COQTOOLSBYTEFLAGS" - ESCBUILDLDPATH="$BUILDLDPATH" - ;; + COQTOP=`echo $COQTOP |sed -e 's|\\\|\\\\\\\|g'` + BINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'` + COQSRC=`cygpath -m $COQSRC |sed -e 's|\\\|\\\\\\\|g'` + LIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'` + CAMLBIN=`echo $CAMLBIN |sed -e 's|\\\|\\\\\\\|g'` + CAMLLIB=`echo $CAMLLIB |sed -e 's|\\\|\\\\\\\|g'` + MANDIR=`echo $MANDIR |sed -e 's|\\\|\\\\\\\|g'` + DOCDIR=`echo $DOCDIR |sed -e 's|\\\|\\\\\\\|g'` + EMACSLIB=`echo $EMACSLIB |sed -e 's|\\\|\\\\\\\|g'` + COQDOCDIR=`echo $COQDOCDIR |sed -e 's|\\\|\\\\\\\|g'` + CAMLP4BIN=`echo $CAMLP4BIN |sed -e 's|\\\|\\\\\\\|g'` + CAMLP4LIB=`echo $CAMLP4LIB |sed -e 's|\\\|\\\\\\\|g'` + LABLGTKINCLUDES=`echo $LABLGTKINCLUDES |sed -e 's|\\\|\\\\\\\|g'` + COQRUNBYTEFLAGS=`echo $COQRUNBYTEFLAGS |sed -e 's|\\\|\\\\\\\|g'` + COQTOOLSBYTEFLAGS=`echo $COQTOOLSBYTEFLAGS |sed -e 's|\\\|\\\\\\\|g'` + BUILDLDPATH=`echo $BUILDLDPATH |sed -e 's|\\\|\\\\\\\|g'` + ocamlexec=`echo $ocamlexec |sed -e 's|\\\|\\\\\\\|g'` + bytecamlc=`echo $bytecamlc |sed -e 's|\\\|\\\\\\\|g'` + nativecamlc=`echo $nativecamlc |sed -e 's|\\\|\\\\\\\|g'` + ocamlmklibexec=`echo $ocamlmklibexec |sed -e 's|\\\|\\\\\\\|g'` + ocamldepexec=`echo $ocamldepexec |sed -e 's|\\\|\\\\\\\|g'` + ocamldocexec=`echo $ocamldocexec |sed -e 's|\\\|\\\\\\\|g'` + ocamllexexec=`echo $ocamllexexec |sed -e 's|\\\|\\\\\\\|g'` + ocamlyaccexec=`echo $ocamlyaccexec |sed -e 's|\\\|\\\\\\\|g'` + camlp4oexec=`echo $camlp4oexec |sed -e 's|\\\|\\\\\\\|g'` + ;; esac -mlconfig_file="$COQSRC/config/coq_config.ml" +##################################################### +# Building the $COQTOP/config/coq_config.ml file +##################################################### + rm -f "$mlconfig_file" cat << END_OF_COQ_CONFIG > $mlconfig_file (* DO NOT EDIT THIS FILE: automatically generated by ../configure *) let local = $local -let coqrunbyteflags = "$ESCCOQRUNBYTEFLAGS" -let coqlib = "$ESCLIBDIR" -let coqsrc = "$ESCSRCDIR" -let camlbin = "$ESCCAMLDIR" -let camllib = "$ESCCAMLLIB" +let coqrunbyteflags = "$COQRUNBYTEFLAGS" +let coqlib = "$LIBDIR" +let coqsrc = "$COQSRC" +let ocaml = "$ocamlexec" +let ocamlc = "$bytecamlc" +let ocamlopt = "$nativecamlc" +let ocamlmklib = "$ocamlmklibexec" +let ocamldep = "$ocamldepexec" +let ocamldoc = "$ocamldocexec" +let ocamlyacc = "$ocamlyaccexec" +let ocamllex = "$ocamllexexec" +let camlbin = "$CAMLBIN" +let camllib = "$CAMLLIB" let camlp4 = "$CAMLP4" -let camlp4bin = "$ESCCAMLP4BIN" -let camlp4lib = "$ESCCAMLP4LIB" +let camlp4o = "$camlp4oexec" +let camlp4bin = "$CAMLP4BIN" +let camlp4lib = "$CAMLP4LIB" +let camlp4compat = "$CAMLP4COMPAT" +let coqideincl = "$LABLGTKINCLUDES" +let cflags = "$cflags" let best = "$best_compiler" let arch = "$ARCH" let has_natdynlink = $HASNATDYNLINK +let natdynlinkflag = "$NATDYNLINKFLAG" let osdeplibs = "$OSDEPLIBS" let version = "$VERSION" let caml_version = "$CAMLVERSION" @@ -956,7 +1005,7 @@ let vo_magic_number = $VOMAGIC let state_magic_number = $STATEMAGIC let exec_extension = "$EXE" let with_geoproof = ref $with_geoproof -let browser = "$ESCBROWSER" +let browser = "$BROWSER" END_OF_COQ_CONFIG @@ -983,32 +1032,32 @@ chmod a-w "$mlconfig_file" # Building the $COQTOP/config/Makefile file ############################################### -rm -f "$COQSRC/config/Makefile" +rm -f "$config_file" sed -e "s|LOCALINSTALLATION|$local|" \ - -e "s|XCOQRUNBYTEFLAGS|$ESCCOQRUNBYTEFLAGS|" \ - -e "s|XCOQTOOLSBYTEFLAGS|$ESCCOQTOOLSBYTEFLAGS|" \ + -e "s|XCOQRUNBYTEFLAGS|$COQRUNBYTEFLAGS|" \ + -e "s|XCOQTOOLSBYTEFLAGS|$COQTOOLSBYTEFLAGS|" \ -e "s|COQSRCDIRECTORY|$COQSRC|" \ -e "s|COQVERSION|$VERSION|" \ - -e "s|BINDIRDIRECTORY|$ESCBINDIR|" \ - -e "s|COQLIBDIRECTORY|$ESCLIBDIR|" \ - -e "s|BUILDLDPATH=|$ESCBUILDLDPATH|" \ - -e "s|MANDIRDIRECTORY|$ESCMANDIR|" \ - -e "s|DOCDIRDIRECTORY|$ESCDOCDIR|" \ - -e "s|EMACSLIBDIRECTORY|$ESCEMACSLIB|" \ + -e "s|BINDIRDIRECTORY|$BINDIR|" \ + -e "s|COQLIBDIRECTORY|$LIBDIR|" \ + -e "s|BUILDLDPATH=|$BUILDLDPATH|" \ + -e "s|MANDIRDIRECTORY|$MANDIR|" \ + -e "s|DOCDIRDIRECTORY|$DOCDIR|" \ + -e "s|EMACSLIBDIRECTORY|$EMACSLIB|" \ -e "s|EMACSCOMMAND|$EMACS|" \ - -e "s|COQDOCDIRECTORY|$ESCCOQDOCDIR|" \ + -e "s|COQDOCDIRECTORY|$COQDOCDIR|" \ -e "s|MKTEXLSRCOMMAND|$MKTEXLSR|" \ -e "s|ARCHITECTURE|$ARCH|" \ -e "s|OSDEPENDENTLIBS|$OSDEPLIBS|" \ -e "s|OSDEPENDENTP4OPTFLAGS|$OSDEPP4OPTFLAGS|" \ - -e "s|CAMLLIBDIRECTORY|$ESCCAMLLIB|" \ + -e "s|CAMLLIBDIRECTORY|$CAMLLIB|" \ -e "s|CAMLTAG|$CAMLTAG|" \ - -e "s|CAMLP4BINDIRECTORY|$ESCCAMLP4BIN|" \ + -e "s|CAMLP4BINDIRECTORY|$CAMLP4BIN|" \ -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \ -e "s|CAMLP4TOOL|$camlp4oexec|" \ -e "s|CAMLP4COMPATFLAGS|$CAMLP4COMPAT|" \ - -e "s|LABLGTKINCLUDES|$ESCLABLGTKINCLUDES|" \ + -e "s|LABLGTKINCLUDES|$LABLGTKINCLUDES|" \ -e "s|COQDEBUGFLAGOPT|$coq_debug_flag_opt|" \ -e "s|COQDEBUGFLAG|$coq_debug_flag|" \ -e "s|COQPROFILEFLAG|$coq_profile_flag|" \ @@ -1036,41 +1085,9 @@ sed -e "s|LOCALINSTALLATION|$local|" \ -e "s|CHECKEDOUTSOURCETREE|$checkedout|" \ -e "s|WITHDOCOPT|$with_doc|" \ -e "s|HASNATIVEDYNLINK|$NATDYNLINKFLAG|" \ - "$COQSRC/config/Makefile.template" > "$COQSRC/config/Makefile" - -chmod a-w "$COQSRC/config/Makefile" - -################################################## -# Building the $COQTOP/dev/ocamldebug-coq file -################################################## + "$config_template" > "$config_file" -OCAMLDEBUGCOQ=$COQSRC/dev/ocamldebug-coq - -if test "$coq_debug_flag" = "-g" ; then - rm -f $OCAMLDEBUGCOQ - sed -e "s|COQTOPDIRECTORY|$COQTOP|" \ - -e "s|COQLIBDIRECTORY|$LIBDIR|" \ - -e "s|CAMLBINDIRECTORY|$CAMLBIN|" \ - -e "s|CAMLP4LIBDIRECTORY|$FULLCAMLP4LIB|"\ - $OCAMLDEBUGCOQ.template > $OCAMLDEBUGCOQ - chmod a-w,a+x $OCAMLDEBUGCOQ -fi - -#################################################### -# Fixing lablgtk types (before/after 2.6.0) -#################################################### - -if [ ! "$COQIDE" = "no" ]; then - if grep "class view " "$lablgtkdir/gText.mli" | grep -q "\[>" ; then - if grep -q "?accepts_tab:bool" "$lablgtkdir/gText.mli" ; then - cp -f ide/undo_lablgtk_ge212.mli ide/undo.mli - else - cp -f ide/undo_lablgtk_ge26.mli ide/undo.mli - fi - else - cp -f ide/undo_lablgtk_lt26.mli ide/undo.mli - fi -fi +chmod a-w "$config_file" ################################################## # The end diff --git a/coq.itarget b/coq.itarget index 72684c23b..7488f421e 100644 --- a/coq.itarget +++ b/coq.itarget @@ -1,2 +1,3 @@ binaries -vo.otarget +plugins/plugins.otarget +theories/theories.otarget diff --git a/myocamlbuild.ml b/myocamlbuild.ml index a16a5e092..432e7ee51 100644 --- a/myocamlbuild.ml +++ b/myocamlbuild.ml @@ -21,68 +21,47 @@ open Scanf *) + (** Generic file reader, which produces a list of strings, one per line *) let read_file f = - let ic = open_in f in - let lines = ref [] in - begin try - while true do lines := (input_line ic)::!lines done - with End_of_file -> () end; - close_in ic; - List.rev !lines - -(** Parse a config file such as config/Makefile. Valid lines are VAR=def. - If def is double-quoted we remove the "..." (first sscanf attempt with %S). - Otherwise, def is as long as possible (%s@\n prevents stopping at ' '). -*) - -let read_env f = - let lines = read_file f in - let add, get = let l = ref [] in (fun x -> l:= x::!l), (fun () -> !l) in - let get_var_def s = - try sscanf s "%[A-Z0-9_]=%S" (fun v d -> add (v,d)) - with _ -> - try sscanf s "%[A-Z0-9_]=%s@\n" (fun v d -> add (v,d)) - with _ -> () - in - List.iter get_var_def lines; get () + let ic = open_in f and l = ref [] in + (try while true do l := (input_line ic)::!l done with End_of_file -> ()); + close_in ic; List.rev !l -let env_vars = - let f = "config/Makefile" in - try read_env f with _ -> (eprintf "Error while reading %s\n" f; exit 1) -let get_env s = - try List.assoc s env_vars - with Not_found -> (eprintf "Unknown environment variable %s\n" s; exit 1) +(** Configuration *) +(** First, we access coq_config.ml indirectly : we symlink it to + myocamlbuild_config.ml, which is linked with this myocamlbuild.ml *) +module Coq_config = struct include Myocamlbuild_config end -(** Configuration *) +let _ = begin + Options.ocamlc := A Coq_config.ocamlc; + Options.ocamlopt := A Coq_config.ocamlopt; + Options.ocamlmklib := A Coq_config.ocamlmklib; + Options.ocamldep := A Coq_config.ocamldep; + Options.ocamldoc := A Coq_config.ocamldoc; + Options.ocamlyacc := A Coq_config.ocamlyacc; + Options.ocamllex := A Coq_config.ocamllex; +end -let _ = Options.ocamlc := A(get_env "OCAMLC") -let _ = Options.ocamlopt := A(get_env "OCAMLOPT") -let _ = Options.ocamlmklib := A(get_env "OCAMLMKLIB") -let _ = Options.ocamldep := A(get_env "OCAMLDEP") -let _ = Options.ocamldoc := A(get_env "OCAMLDOC") -let _ = Options.ocamlopt := A(get_env "OCAMLOPT") -let _ = Options.ocamlyacc := A(get_env "OCAMLYACC") -let _ = Options.ocamllex := A(get_env "OCAMLLEX") - -let ocaml = A(get_env "OCAML") -let camlp4o = A(get_env "CAMLP4O") -let camlp4incl = S[A"-I"; A(get_env "MYCAMLP4LIB")] -let camlp4compat = Sh(get_env "CAMLP4COMPAT") -let opt = (get_env "BEST" = "opt") +let ocaml = A Coq_config.ocaml +let camlp4o = A Coq_config.camlp4o +let camlp4incl = S[A"-I"; A Coq_config.camlp4lib] +let camlp4compat = Sh Coq_config.camlp4compat +let opt = (Coq_config.best = "opt") let best_oext = if opt then ".native" else ".byte" let best_ext = if opt then ".opt" else ".byte" -let hasdynlink = (get_env "HASNATDYNLINK" <> "false") -let os5fix = (get_env "HASNATDYNLINK" = "os5fixme") +let hasdynlink = Coq_config.has_natdynlink +let os5fix = (Coq_config.natdynlinkflag = "os5fixme") let flag_dynlink = if hasdynlink then A"-DHasDynlink" else N let dep_dynlink = if hasdynlink then N else Sh"-natdynlink no" -let lablgtkincl = Sh(get_env "COQIDEINCLUDES") -let local = (get_env "LOCAL" = "true") -let coqsrc = get_env "COQSRC" +let lablgtkincl = Sh Coq_config.coqideincl +let local = Coq_config.local +let coqsrc = Coq_config.coqsrc +let cflags = S[A"-ccopt";A Coq_config.cflags] (** Do we want to inspect .ml generated from .ml4 ? *) let readable_genml = false @@ -130,7 +109,22 @@ let makeinitial = "states/MakeInitial.v" let nmake = "theories/Numbers/Natural/BigN/NMake.v" let nmakegen = "theories/Numbers/Natural/BigN/NMake_gen.ml" -let genvfiles = [nmake] +let theoriesv = + let vo = string_list_of_file "theories/theories.itarget" in + List.map (fun s -> "theories/"^(Filename.chop_suffix s "o")) vo + +let contribv = + let vo = string_list_of_file "plugins/pluginsvo.itarget" in + List.map (fun s -> "plugins/"^(Filename.chop_suffix s "o")) vo + +let contribmllib = + let cma = string_list_of_file "plugins/pluginsbyte.itarget" in + List.map (fun s -> "plugins/"^(Filename.chop_suffix s ".cma")^".mllib") cma + +(** for correct execution of coqdep_boot, source files should have + been imported in _build (and NMake.v should have been created). *) + +let coqdepdeps = theoriesv @ contribv @ contribmllib let coqtop = "toplevel/coqtop" let coqide = "ide/coqide" @@ -140,19 +134,22 @@ let coqmktop = "scripts/coqmktop" (** The list of binaries to build: (name of link in bin/, name in _build, install both or only best) *) +type links = Both | Best | BestInPlace + let all_binaries = - [ "coqtop", coqtop, true; - "coqide", coqide, true; - "coqmktop", coqmktop, true; - "coqc", "scripts/coqc", true; - "coqchk", "checker/main", true; - "coqdep_boot", coqdepboot, false; - "coqdep", "tools/coqdep", false; - "coqdoc", "tools/coqdoc/main", false; - "coqwc", "tools/coqwc", false; - "coq_makefile", "tools/coq_makefile", false; - "coq-tex", "tools/coq_tex", false; - "gallina", "tools/gallina", false; + [ "coqtop", coqtop, Both; + "coqide", coqide, Both; + "coqmktop", coqmktop, Both; + "coqc", "scripts/coqc", Both; + "coqchk", "checker/main", Both; + "coqdep_boot", coqdepboot, Best; + "coqdep", "tools/coqdep", Best; + "coqdoc", "tools/coqdoc/main", Best; + "coqwc", "tools/coqwc", Best; + "coq_makefile", "tools/coq_makefile", Best; + "coq-tex", "tools/coq_tex", Best; + "gallina", "tools/gallina", Best; + "csdpcert", "plugins/micromega/csdpcert", BestInPlace; ] let coqtopbest = coqtop^best_oext @@ -162,8 +159,8 @@ let coqmktopbest = coqmktop^best_oext let binaries_deps = let rec deps = function | [] -> [] - | (_,bin,both) :: l -> - if opt && both then (bin^".native") :: (bin^".byte") :: deps l + | (_,bin,kind) :: l -> + if opt && kind=Both then (bin^".native") :: (bin^".byte") :: deps l else (bin^best_oext) :: deps l in deps all_binaries @@ -172,14 +169,17 @@ let ln_sf toward f = let rec make_bin_links = function | [] -> () - | (b,ob,true) :: l -> + | (b,ob,Both) :: l -> ln_sf ("../"^ !_build^"/"^ob^".byte") ("bin/"^b^".byte"); if opt then ln_sf ("../"^ !_build^"/"^ob^".native") ("bin/"^b^".opt"); ln_sf (b^best_ext) ("bin/"^b); make_bin_links l - | (b,ob,false) :: l -> + | (b,ob,Best) :: l -> ln_sf ("../"^ !_build^"/"^ob^best_oext) ("bin/"^b); make_bin_links l + | (b,ob,BestInPlace) :: l -> + ln_sf (b^best_oext) ob; + make_bin_links l let incl f = Ocaml_utils.ocaml_include_flags f @@ -189,14 +189,6 @@ let initial_actions () = begin make_bin_links all_binaries; (** We "pre-create" a few subdirs in _build to please coqtop *) Shell.mkdir_p (!_build^"/dev"); - (** Moreover, we "pre-import" in _build the sources file that will be needed - by coqdep_boot *) - (*TODO: do something nicer than this call to find (maybe with Slurp) *) - let exclude = "-name _\\$* -or -name .\\* -prune -or" in - Command.execute ~quiet:true (Cmd (Sh - ("for i in `find theories plugins "^exclude^" -print`; do "^ - "[ -f $i -a ! -f _build/$i ] && mkdir -p _build/`dirname $i` && cp $i _build/$i; "^ - "done; true"))) end let extra_rules () = begin @@ -275,7 +267,7 @@ let extra_rules () = begin (** C code for the VM *) dep ["compile"; "c"] c_headers; - flag ["compile"; "c"] (S[A"-ccopt";A"-fno-defer-pop -Wall -Wno-unused"]); + flag ["compile"; "c"] cflags; dep ["link"; "ocaml"; "use_libcoqrun"] [libcoqrun]; (** VM: Generation of coq_jumbtbl.h and copcodes.ml from coq_instruct.h *) @@ -334,7 +326,9 @@ let extra_rules () = begin (** Coq files dependencies *) - rule ".v.d" ~prod:"%.v.depends" ~deps:(["%.v";coqdepbest]@genvfiles) + rule "coqdepready" ~stamp:"coqdepready" ~deps:coqdepdeps (fun _ _ -> Nop); + + rule ".v.d" ~prod:"%.v.depends" ~deps:["%.v";coqdepbest;"coqdepready"] (fun env _ -> let v = env "%.v" and vd = env "%.v.depends" in (** NB: this relies on all .v files being already in _build. *) diff --git a/plugins/plugins.itarget b/plugins/plugins.itarget new file mode 100644 index 000000000..56aa42b06 --- /dev/null +++ b/plugins/plugins.itarget @@ -0,0 +1,3 @@ +pluginsopt.otarget +pluginsbyte.otarget +pluginsvo.otarget \ No newline at end of file diff --git a/plugins/pluginsbyte.itarget b/plugins/pluginsbyte.itarget new file mode 100644 index 000000000..7e0a77787 --- /dev/null +++ b/plugins/pluginsbyte.itarget @@ -0,0 +1,25 @@ +field/field_plugin.cma +setoid_ring/newring_plugin.cma +extraction/extraction_plugin.cma +firstorder/ground_plugin.cma +rtauto/rtauto_plugin.cma +interface/coqinterface_plugin.cma +interface/coqparser_plugin.cma +fourier/fourier_plugin.cma +romega/romega_plugin.cma +omega/omega_plugin.cma +micromega/micromega_plugin.cma +dp/dp_plugin.cma +xml/xml_plugin.cma +subtac/subtac_plugin.cma +ring/ring_plugin.cma +cc/cc_plugin.cma +groebner/groebner_plugin.cma +funind/recdef_plugin.cma +syntax/ascii_syntax_plugin.cma +syntax/nat_syntax_plugin.cma +syntax/numbers_syntax_plugin.cma +syntax/r_syntax_plugin.cma +syntax/string_syntax_plugin.cma +syntax/z_syntax_plugin.cma +quote/quote_plugin.cma diff --git a/plugins/pluginsopt.itarget b/plugins/pluginsopt.itarget new file mode 100644 index 000000000..e8e7868b7 --- /dev/null +++ b/plugins/pluginsopt.itarget @@ -0,0 +1,25 @@ +field/field_plugin.cmxa +setoid_ring/newring_plugin.cmxa +extraction/extraction_plugin.cmxa +firstorder/ground_plugin.cmxa +rtauto/rtauto_plugin.cmxa +interface/coqinterface_plugin.cmxa +interface/coqparser_plugin.cmxa +fourier/fourier_plugin.cmxa +romega/romega_plugin.cmxa +omega/omega_plugin.cmxa +micromega/micromega_plugin.cmxa +dp/dp_plugin.cmxa +xml/xml_plugin.cmxa +subtac/subtac_plugin.cmxa +ring/ring_plugin.cmxa +cc/cc_plugin.cmxa +groebner/groebner_plugin.cmxa +funind/recdef_plugin.cmxa +syntax/ascii_syntax_plugin.cmxa +syntax/nat_syntax_plugin.cmxa +syntax/numbers_syntax_plugin.cmxa +syntax/r_syntax_plugin.cmxa +syntax/string_syntax_plugin.cmxa +syntax/z_syntax_plugin.cmxa +quote/quote_plugin.cmxa diff --git a/plugins/pluginsvo.itarget b/plugins/pluginsvo.itarget new file mode 100644 index 000000000..af4d23310 --- /dev/null +++ b/plugins/pluginsvo.itarget @@ -0,0 +1,60 @@ +dp/Dp.vo +field/LegacyField_Compl.vo +field/LegacyField_Tactic.vo +field/LegacyField_Theory.vo +field/LegacyField.vo +fourier/Fourier_util.vo +fourier/Fourier.vo +funind/Recdef.vo +groebner/GroebnerR.vo +groebner/GroebnerZ.vo +interface/CoqInterface.vo +#interface/CoqParser.vo (should not be compiled) +micromega/CheckerMaker.vo +micromega/EnvRing.vo +micromega/Env.vo +#micromega/MExtraction.vo (extraction of micromega.ml) +micromega/OrderedRing.vo +micromega/Psatz.vo +micromega/QMicromega.vo +micromega/Refl.vo +micromega/RingMicromega.vo +micromega/RMicromega.vo +micromega/Tauto.vo +micromega/VarMap.vo +micromega/ZCoeff.vo +micromega/ZMicromega.vo +omega/OmegaLemmas.vo +omega/OmegaPlugin.vo +omega/Omega.vo +omega/PreOmega.vo +quote/Quote.vo +ring/LegacyArithRing.vo +ring/LegacyNArithRing.vo +ring/LegacyRing_theory.vo +ring/LegacyRing.vo +ring/LegacyZArithRing.vo +ring/Ring_abstract.vo +ring/Ring_normalize.vo +ring/Setoid_ring_normalize.vo +ring/Setoid_ring_theory.vo +ring/Setoid_ring.vo +romega/ReflOmegaCore.vo +romega/ROmega.vo +rtauto/Bintree.vo +rtauto/Rtauto.vo +setoid_ring/ArithRing.vo +setoid_ring/BinList.vo +setoid_ring/Field_tac.vo +setoid_ring/Field_theory.vo +setoid_ring/Field.vo +setoid_ring/InitialRing.vo +setoid_ring/NArithRing.vo +setoid_ring/RealField.vo +setoid_ring/Ring_base.vo +setoid_ring/Ring_equiv.vo +setoid_ring/Ring_polynom.vo +setoid_ring/Ring_tac.vo +setoid_ring/Ring_theory.vo +setoid_ring/Ring.vo +setoid_ring/ZArithRing.vo diff --git a/theories/theories.itarget b/theories/theories.itarget new file mode 100644 index 000000000..7798ebebc --- /dev/null +++ b/theories/theories.itarget @@ -0,0 +1,348 @@ +Arith/Arith_base.vo +Arith/Arith.vo +Arith/Between.vo +Arith/Bool_nat.vo +Arith/Compare_dec.vo +Arith/Compare.vo +Arith/Div2.vo +Arith/EqNat.vo +Arith/Euclid.vo +Arith/Even.vo +Arith/Factorial.vo +Arith/Gt.vo +Arith/Le.vo +Arith/Lt.vo +Arith/Max.vo +Arith/Minus.vo +Arith/Min.vo +Arith/Mult.vo +Arith/Peano_dec.vo +Arith/Plus.vo +Arith/Wf_nat.vo + +Bool/BoolEq.vo +Bool/Bool.vo +Bool/Bvector.vo +Bool/DecBool.vo +Bool/IfProp.vo +Bool/Sumbool.vo +Bool/Zerob.vo + +Classes/Equivalence.vo +Classes/EquivDec.vo +Classes/Functions.vo +Classes/Init.vo +Classes/Morphisms_Prop.vo +Classes/Morphisms_Relations.vo +Classes/Morphisms.vo +Classes/RelationClasses.vo +Classes/SetoidAxioms.vo +Classes/SetoidClass.vo +Classes/SetoidDec.vo +Classes/SetoidTactics.vo + +FSets/FMapAVL.vo +FSets/FMapFacts.vo +FSets/FMapFullAVL.vo +FSets/FMapInterface.vo +FSets/FMapList.vo +FSets/FMapPositive.vo +FSets/FMaps.vo +FSets/FMapWeakList.vo +FSets/FSetAVL.vo +FSets/FSetBridge.vo +FSets/FSetDecide.vo +FSets/FSetEqProperties.vo +FSets/FSetFacts.vo +FSets/FSetFullAVL.vo +FSets/FSetInterface.vo +FSets/FSetList.vo +FSets/FSetProperties.vo +FSets/FSets.vo +FSets/FSetToFiniteSet.vo +FSets/FSetWeakList.vo +FSets/OrderedTypeAlt.vo +FSets/OrderedTypeEx.vo +FSets/OrderedType.vo + +Init/Datatypes.vo +Init/Logic_Type.vo +Init/Logic.vo +Init/Notations.vo +Init/Peano.vo +Init/Prelude.vo +Init/Specif.vo +Init/Tactics.vo +Init/Wf.vo + +Lists/ListSet.vo +Lists/ListTactics.vo +Lists/List.vo +Lists/MonoList.vo +Lists/SetoidList.vo +Lists/StreamMemo.vo +Lists/Streams.vo +Lists/TheoryList.vo + +Logic/Berardi.vo +Logic/ChoiceFacts.vo +Logic/ClassicalChoice.vo +Logic/ClassicalDescription.vo +Logic/ClassicalEpsilon.vo +Logic/ClassicalFacts.vo +Logic/Classical_Pred_Set.vo +Logic/Classical_Pred_Type.vo +Logic/Classical_Prop.vo +Logic/Classical_Type.vo +Logic/ClassicalUniqueChoice.vo +Logic/Classical.vo +Logic/ConstructiveEpsilon.vo +Logic/DecidableTypeEx.vo +Logic/DecidableType.vo +Logic/Decidable.vo +Logic/Description.vo +Logic/Diaconescu.vo +Logic/Epsilon.vo +Logic/Eqdep_dec.vo +Logic/EqdepFacts.vo +Logic/Eqdep.vo +Logic/FunctionalExtensionality.vo +Logic/Hurkens.vo +Logic/IndefiniteDescription.vo +Logic/JMeq.vo +Logic/ProofIrrelevanceFacts.vo +Logic/ProofIrrelevance.vo +Logic/RelationalChoice.vo +Logic/SetIsType.vo + +NArith/BinNat.vo +NArith/BinPos.vo +NArith/NArith.vo +NArith/Ndec.vo +NArith/Ndigits.vo +NArith/Ndist.vo +NArith/Nnat.vo +NArith/Pnat.vo + +Numbers/BigNumPrelude.vo +Numbers/Cyclic/Abstract/CyclicAxioms.vo +Numbers/Cyclic/Abstract/NZCyclic.vo +Numbers/Cyclic/DoubleCyclic/DoubleAdd.vo +Numbers/Cyclic/DoubleCyclic/DoubleBase.vo +Numbers/Cyclic/DoubleCyclic/DoubleCyclic.vo +Numbers/Cyclic/DoubleCyclic/DoubleDivn1.vo +Numbers/Cyclic/DoubleCyclic/DoubleDiv.vo +Numbers/Cyclic/DoubleCyclic/DoubleLift.vo +Numbers/Cyclic/DoubleCyclic/DoubleMul.vo +Numbers/Cyclic/DoubleCyclic/DoubleSqrt.vo +Numbers/Cyclic/DoubleCyclic/DoubleSub.vo +Numbers/Cyclic/DoubleCyclic/DoubleType.vo +Numbers/Cyclic/Int31/Cyclic31.vo +Numbers/Cyclic/Int31/Int31.vo +Numbers/Cyclic/ZModulo/ZModulo.vo +Numbers/Integer/Abstract/ZAddOrder.vo +Numbers/Integer/Abstract/ZAdd.vo +Numbers/Integer/Abstract/ZAxioms.vo +Numbers/Integer/Abstract/ZBase.vo +#Numbers/Integer/Abstract/ZDomain.vo +Numbers/Integer/Abstract/ZLt.vo +Numbers/Integer/Abstract/ZMulOrder.vo +Numbers/Integer/Abstract/ZMul.vo +Numbers/Integer/BigZ/BigZ.vo +Numbers/Integer/BigZ/ZMake.vo +Numbers/Integer/Binary/ZBinary.vo +Numbers/Integer/NatPairs/ZNatPairs.vo +Numbers/Integer/SpecViaZ/ZSig.vo +Numbers/Integer/SpecViaZ/ZSigZAxioms.vo +Numbers/NaryFunctions.vo +Numbers/NatInt/NZAddOrder.vo +Numbers/NatInt/NZAdd.vo +Numbers/NatInt/NZAxioms.vo +Numbers/NatInt/NZBase.vo +Numbers/NatInt/NZMulOrder.vo +Numbers/NatInt/NZMul.vo +Numbers/NatInt/NZOrder.vo +Numbers/Natural/Abstract/NAddOrder.vo +Numbers/Natural/Abstract/NAdd.vo +Numbers/Natural/Abstract/NAxioms.vo +Numbers/Natural/Abstract/NBase.vo +#Numbers/Natural/Abstract/NDefOps.vo +Numbers/Natural/Abstract/NIso.vo +Numbers/Natural/Abstract/NMulOrder.vo +Numbers/Natural/Abstract/NMul.vo +Numbers/Natural/Abstract/NOrder.vo +#Numbers/Natural/Abstract/NStrongRec.vo +Numbers/Natural/Abstract/NSub.vo +Numbers/Natural/BigN/BigN.vo +Numbers/Natural/BigN/Nbasic.vo +# Beware: source file for the next one is generated by a script +Numbers/Natural/BigN/NMake.vo +Numbers/Natural/Binary/NBinary.vo +Numbers/Natural/Binary/NBinDefs.vo +Numbers/Natural/Peano/NPeano.vo +Numbers/Natural/SpecViaZ/NSigNAxioms.vo +Numbers/Natural/SpecViaZ/NSig.vo +Numbers/NumPrelude.vo +Numbers/Rational/BigQ/BigQ.vo +Numbers/Rational/BigQ/QMake.vo +Numbers/Rational/SpecViaQ/QSig.vo + +Program/Basics.vo +Program/Combinators.vo +Program/Equality.vo +Program/Program.vo +Program/Subset.vo +Program/Syntax.vo +Program/Tactics.vo +Program/Utils.vo +Program/Wf.vo + +QArith/Qabs.vo +QArith/QArith_base.vo +QArith/QArith.vo +QArith/Qcanon.vo +QArith/Qfield.vo +QArith/Qpower.vo +QArith/Qreals.vo +QArith/Qreduction.vo +QArith/Qring.vo +QArith/Qround.vo + +Reals/Alembert.vo +Reals/AltSeries.vo +Reals/ArithProp.vo +Reals/Binomial.vo +Reals/Cauchy_prod.vo +Reals/Cos_plus.vo +Reals/Cos_rel.vo +Reals/DiscrR.vo +Reals/Exp_prop.vo +Reals/Integration.vo +Reals/LegacyRfield.vo +Reals/MVT.vo +Reals/NewtonInt.vo +Reals/PartSum.vo +Reals/PSeries_reg.vo +Reals/Ranalysis1.vo +Reals/Ranalysis2.vo +Reals/Ranalysis3.vo +Reals/Ranalysis4.vo +Reals/Ranalysis.vo +Reals/Raxioms.vo +Reals/Rbase.vo +Reals/Rbasic_fun.vo +Reals/Rcomplete.vo +Reals/Rdefinitions.vo +Reals/Rderiv.vo +Reals/Reals.vo +Reals/Rfunctions.vo +Reals/Rgeom.vo +Reals/RiemannInt_SF.vo +Reals/RiemannInt.vo +Reals/R_Ifp.vo +Reals/RIneq.vo +Reals/Rlimit.vo +Reals/RList.vo +Reals/Rlogic.vo +Reals/Rpow_def.vo +Reals/Rpower.vo +Reals/Rprod.vo +Reals/Rseries.vo +Reals/Rsigma.vo +Reals/Rsqrt_def.vo +Reals/R_sqrt.vo +Reals/R_sqr.vo +Reals/Rtopology.vo +Reals/Rtrigo_alt.vo +Reals/Rtrigo_calc.vo +Reals/Rtrigo_def.vo +Reals/Rtrigo_fun.vo +Reals/Rtrigo_reg.vo +Reals/Rtrigo.vo +Reals/SeqProp.vo +Reals/SeqSeries.vo +Reals/SplitAbsolu.vo +Reals/SplitRmult.vo +Reals/Sqrt_reg.vo + +Relations/Operators_Properties.vo +Relations/Relation_Definitions.vo +Relations/Relation_Operators.vo +Relations/Relations.vo + +Setoids/Setoid.vo +Sets/Classical_sets.vo +Sets/Constructive_sets.vo +Sets/Cpo.vo +Sets/Ensembles.vo +Sets/Finite_sets_facts.vo +Sets/Finite_sets.vo +Sets/Image.vo +Sets/Infinite_sets.vo +Sets/Integers.vo +Sets/Multiset.vo +Sets/Partial_Order.vo +Sets/Permut.vo +Sets/Powerset_Classical_facts.vo +Sets/Powerset_facts.vo +Sets/Powerset.vo +Sets/Relations_1_facts.vo +Sets/Relations_1.vo +Sets/Relations_2_facts.vo +Sets/Relations_2.vo +Sets/Relations_3_facts.vo +Sets/Relations_3.vo +Sets/Uniset.vo + +Sorting/Heap.vo +Sorting/Permutation.vo +Sorting/PermutEq.vo +Sorting/PermutSetoid.vo +Sorting/Sorting.vo + +Strings/Ascii.vo +Strings/String.vo + +Unicode/Utf8.vo + +Wellfounded/Disjoint_Union.vo +Wellfounded/Inclusion.vo +Wellfounded/Inverse_Image.vo +Wellfounded/Lexicographic_Exponentiation.vo +Wellfounded/Lexicographic_Product.vo +Wellfounded/Transitive_Closure.vo +Wellfounded/Union.vo +Wellfounded/Wellfounded.vo +Wellfounded/Well_Ordering.vo + +ZArith/auxiliary.vo +ZArith/BinInt.vo +ZArith/Int.vo +ZArith/Wf_Z.vo +ZArith/Zabs.vo +ZArith/ZArith_base.vo +ZArith/ZArith_dec.vo +ZArith/ZArith.vo +ZArith/Zbinary.vo +ZArith/Zbool.vo +ZArith/Zcompare.vo +ZArith/Zcomplements.vo +ZArith/Zdiv.vo +ZArith/Zeven.vo +ZArith/Zgcd_alt.vo +ZArith/Zhints.vo +ZArith/Zlogarithm.vo +ZArith/Zmax.vo +ZArith/Zminmax.vo +ZArith/Zmin.vo +ZArith/Zmisc.vo +ZArith/Znat.vo +ZArith/Znumtheory.vo +ZArith/ZOdiv_def.vo +ZArith/ZOdiv.vo +ZArith/Zorder.vo +ZArith/Zpow_def.vo +ZArith/Zpower.vo +ZArith/Zpow_facts.vo +ZArith/Zsqrt.vo +ZArith/Zwf.vo diff --git a/vo.itarget b/vo.itarget deleted file mode 100644 index 8898dd8fa..000000000 --- a/vo.itarget +++ /dev/null @@ -1,407 +0,0 @@ -theories/Arith/Arith_base.vo -theories/Arith/Arith.vo -theories/Arith/Between.vo -theories/Arith/Bool_nat.vo -theories/Arith/Compare_dec.vo -theories/Arith/Compare.vo -theories/Arith/Div2.vo -theories/Arith/EqNat.vo -theories/Arith/Euclid.vo -theories/Arith/Even.vo -theories/Arith/Factorial.vo -theories/Arith/Gt.vo -theories/Arith/Le.vo -theories/Arith/Lt.vo -theories/Arith/Max.vo -theories/Arith/Minus.vo -theories/Arith/Min.vo -theories/Arith/Mult.vo -theories/Arith/Peano_dec.vo -theories/Arith/Plus.vo -theories/Arith/Wf_nat.vo - -theories/Bool/BoolEq.vo -theories/Bool/Bool.vo -theories/Bool/Bvector.vo -theories/Bool/DecBool.vo -theories/Bool/IfProp.vo -theories/Bool/Sumbool.vo -theories/Bool/Zerob.vo - -theories/Classes/Equivalence.vo -theories/Classes/EquivDec.vo -theories/Classes/Functions.vo -theories/Classes/Init.vo -theories/Classes/Morphisms_Prop.vo -theories/Classes/Morphisms_Relations.vo -theories/Classes/Morphisms.vo -theories/Classes/RelationClasses.vo -theories/Classes/SetoidAxioms.vo -theories/Classes/SetoidClass.vo -theories/Classes/SetoidDec.vo -theories/Classes/SetoidTactics.vo - -theories/FSets/FMapAVL.vo -theories/FSets/FMapFacts.vo -theories/FSets/FMapFullAVL.vo -theories/FSets/FMapInterface.vo -theories/FSets/FMapList.vo -theories/FSets/FMapPositive.vo -theories/FSets/FMaps.vo -theories/FSets/FMapWeakList.vo -theories/FSets/FSetAVL.vo -theories/FSets/FSetBridge.vo -theories/FSets/FSetDecide.vo -theories/FSets/FSetEqProperties.vo -theories/FSets/FSetFacts.vo -theories/FSets/FSetFullAVL.vo -theories/FSets/FSetInterface.vo -theories/FSets/FSetList.vo -theories/FSets/FSetProperties.vo -theories/FSets/FSets.vo -theories/FSets/FSetToFiniteSet.vo -theories/FSets/FSetWeakList.vo -theories/FSets/OrderedTypeAlt.vo -theories/FSets/OrderedTypeEx.vo -theories/FSets/OrderedType.vo - -theories/Init/Datatypes.vo -theories/Init/Logic_Type.vo -theories/Init/Logic.vo -theories/Init/Notations.vo -theories/Init/Peano.vo -theories/Init/Prelude.vo -theories/Init/Specif.vo -theories/Init/Tactics.vo -theories/Init/Wf.vo - -theories/Lists/ListSet.vo -theories/Lists/ListTactics.vo -theories/Lists/List.vo -theories/Lists/MonoList.vo -theories/Lists/SetoidList.vo -theories/Lists/StreamMemo.vo -theories/Lists/Streams.vo -theories/Lists/TheoryList.vo - -theories/Logic/Berardi.vo -theories/Logic/ChoiceFacts.vo -theories/Logic/ClassicalChoice.vo -theories/Logic/ClassicalDescription.vo -theories/Logic/ClassicalEpsilon.vo -theories/Logic/ClassicalFacts.vo -theories/Logic/Classical_Pred_Set.vo -theories/Logic/Classical_Pred_Type.vo -theories/Logic/Classical_Prop.vo -theories/Logic/Classical_Type.vo -theories/Logic/ClassicalUniqueChoice.vo -theories/Logic/Classical.vo -theories/Logic/ConstructiveEpsilon.vo -theories/Logic/DecidableTypeEx.vo -theories/Logic/DecidableType.vo -theories/Logic/Decidable.vo -theories/Logic/Description.vo -theories/Logic/Diaconescu.vo -theories/Logic/Epsilon.vo -theories/Logic/Eqdep_dec.vo -theories/Logic/EqdepFacts.vo -theories/Logic/Eqdep.vo -theories/Logic/FunctionalExtensionality.vo -theories/Logic/Hurkens.vo -theories/Logic/IndefiniteDescription.vo -theories/Logic/JMeq.vo -theories/Logic/ProofIrrelevanceFacts.vo -theories/Logic/ProofIrrelevance.vo -theories/Logic/RelationalChoice.vo -theories/Logic/SetIsType.vo - -theories/NArith/BinNat.vo -theories/NArith/BinPos.vo -theories/NArith/NArith.vo -theories/NArith/Ndec.vo -theories/NArith/Ndigits.vo -theories/NArith/Ndist.vo -theories/NArith/Nnat.vo -theories/NArith/Pnat.vo - -theories/Numbers/BigNumPrelude.vo -theories/Numbers/Cyclic/Abstract/CyclicAxioms.vo -theories/Numbers/Cyclic/Abstract/NZCyclic.vo -theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.vo -theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.vo -theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.vo -theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.vo -theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.vo -theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.vo -theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.vo -theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.vo -theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.vo -theories/Numbers/Cyclic/DoubleCyclic/DoubleType.vo -theories/Numbers/Cyclic/Int31/Cyclic31.vo -theories/Numbers/Cyclic/Int31/Int31.vo -theories/Numbers/Cyclic/ZModulo/ZModulo.vo -theories/Numbers/Integer/Abstract/ZAddOrder.vo -theories/Numbers/Integer/Abstract/ZAdd.vo -theories/Numbers/Integer/Abstract/ZAxioms.vo -theories/Numbers/Integer/Abstract/ZBase.vo -#theories/Numbers/Integer/Abstract/ZDomain.vo -theories/Numbers/Integer/Abstract/ZLt.vo -theories/Numbers/Integer/Abstract/ZMulOrder.vo -theories/Numbers/Integer/Abstract/ZMul.vo -theories/Numbers/Integer/BigZ/BigZ.vo -theories/Numbers/Integer/BigZ/ZMake.vo -theories/Numbers/Integer/Binary/ZBinary.vo -theories/Numbers/Integer/NatPairs/ZNatPairs.vo -theories/Numbers/Integer/SpecViaZ/ZSig.vo -theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.vo -theories/Numbers/NaryFunctions.vo -theories/Numbers/NatInt/NZAddOrder.vo -theories/Numbers/NatInt/NZAdd.vo -theories/Numbers/NatInt/NZAxioms.vo -theories/Numbers/NatInt/NZBase.vo -theories/Numbers/NatInt/NZMulOrder.vo -theories/Numbers/NatInt/NZMul.vo -theories/Numbers/NatInt/NZOrder.vo -theories/Numbers/Natural/Abstract/NAddOrder.vo -theories/Numbers/Natural/Abstract/NAdd.vo -theories/Numbers/Natural/Abstract/NAxioms.vo -theories/Numbers/Natural/Abstract/NBase.vo -#theories/Numbers/Natural/Abstract/NDefOps.vo -theories/Numbers/Natural/Abstract/NIso.vo -theories/Numbers/Natural/Abstract/NMulOrder.vo -theories/Numbers/Natural/Abstract/NMul.vo -theories/Numbers/Natural/Abstract/NOrder.vo -#theories/Numbers/Natural/Abstract/NStrongRec.vo -theories/Numbers/Natural/Abstract/NSub.vo -theories/Numbers/Natural/BigN/BigN.vo -theories/Numbers/Natural/BigN/Nbasic.vo -theories/Numbers/Natural/Binary/NBinary.vo -theories/Numbers/Natural/Binary/NBinDefs.vo -theories/Numbers/Natural/Peano/NPeano.vo -theories/Numbers/Natural/SpecViaZ/NSigNAxioms.vo -theories/Numbers/Natural/SpecViaZ/NSig.vo -theories/Numbers/NumPrelude.vo -theories/Numbers/Rational/BigQ/BigQ.vo -theories/Numbers/Rational/BigQ/QMake.vo -theories/Numbers/Rational/SpecViaQ/QSig.vo - -theories/Program/Basics.vo -theories/Program/Combinators.vo -theories/Program/Equality.vo -theories/Program/Program.vo -theories/Program/Subset.vo -theories/Program/Syntax.vo -theories/Program/Tactics.vo -theories/Program/Utils.vo -theories/Program/Wf.vo - -theories/QArith/Qabs.vo -theories/QArith/QArith_base.vo -theories/QArith/QArith.vo -theories/QArith/Qcanon.vo -theories/QArith/Qfield.vo -theories/QArith/Qpower.vo -theories/QArith/Qreals.vo -theories/QArith/Qreduction.vo -theories/QArith/Qring.vo -theories/QArith/Qround.vo - -theories/Reals/Alembert.vo -theories/Reals/AltSeries.vo -theories/Reals/ArithProp.vo -theories/Reals/Binomial.vo -theories/Reals/Cauchy_prod.vo -theories/Reals/Cos_plus.vo -theories/Reals/Cos_rel.vo -theories/Reals/DiscrR.vo -theories/Reals/Exp_prop.vo -theories/Reals/Integration.vo -theories/Reals/LegacyRfield.vo -theories/Reals/MVT.vo -theories/Reals/NewtonInt.vo -theories/Reals/PartSum.vo -theories/Reals/PSeries_reg.vo -theories/Reals/Ranalysis1.vo -theories/Reals/Ranalysis2.vo -theories/Reals/Ranalysis3.vo -theories/Reals/Ranalysis4.vo -theories/Reals/Ranalysis.vo -theories/Reals/Raxioms.vo -theories/Reals/Rbase.vo -theories/Reals/Rbasic_fun.vo -theories/Reals/Rcomplete.vo -theories/Reals/Rdefinitions.vo -theories/Reals/Rderiv.vo -theories/Reals/Reals.vo -theories/Reals/Rfunctions.vo -theories/Reals/Rgeom.vo -theories/Reals/RiemannInt_SF.vo -theories/Reals/RiemannInt.vo -theories/Reals/R_Ifp.vo -theories/Reals/RIneq.vo -theories/Reals/Rlimit.vo -theories/Reals/RList.vo -theories/Reals/Rlogic.vo -theories/Reals/Rpow_def.vo -theories/Reals/Rpower.vo -theories/Reals/Rprod.vo -theories/Reals/Rseries.vo -theories/Reals/Rsigma.vo -theories/Reals/Rsqrt_def.vo -theories/Reals/R_sqrt.vo -theories/Reals/R_sqr.vo -theories/Reals/Rtopology.vo -theories/Reals/Rtrigo_alt.vo -theories/Reals/Rtrigo_calc.vo -theories/Reals/Rtrigo_def.vo -theories/Reals/Rtrigo_fun.vo -theories/Reals/Rtrigo_reg.vo -theories/Reals/Rtrigo.vo -theories/Reals/SeqProp.vo -theories/Reals/SeqSeries.vo -theories/Reals/SplitAbsolu.vo -theories/Reals/SplitRmult.vo -theories/Reals/Sqrt_reg.vo - -theories/Relations/Operators_Properties.vo -theories/Relations/Relation_Definitions.vo -theories/Relations/Relation_Operators.vo -theories/Relations/Relations.vo - -theories/Setoids/Setoid.vo -theories/Sets/Classical_sets.vo -theories/Sets/Constructive_sets.vo -theories/Sets/Cpo.vo -theories/Sets/Ensembles.vo -theories/Sets/Finite_sets_facts.vo -theories/Sets/Finite_sets.vo -theories/Sets/Image.vo -theories/Sets/Infinite_sets.vo -theories/Sets/Integers.vo -theories/Sets/Multiset.vo -theories/Sets/Partial_Order.vo -theories/Sets/Permut.vo -theories/Sets/Powerset_Classical_facts.vo -theories/Sets/Powerset_facts.vo -theories/Sets/Powerset.vo -theories/Sets/Relations_1_facts.vo -theories/Sets/Relations_1.vo -theories/Sets/Relations_2_facts.vo -theories/Sets/Relations_2.vo -theories/Sets/Relations_3_facts.vo -theories/Sets/Relations_3.vo -theories/Sets/Uniset.vo - -theories/Sorting/Heap.vo -theories/Sorting/Permutation.vo -theories/Sorting/PermutEq.vo -theories/Sorting/PermutSetoid.vo -theories/Sorting/Sorting.vo - -theories/Strings/Ascii.vo -theories/Strings/String.vo - -theories/Unicode/Utf8.vo - -theories/Wellfounded/Disjoint_Union.vo -theories/Wellfounded/Inclusion.vo -theories/Wellfounded/Inverse_Image.vo -theories/Wellfounded/Lexicographic_Exponentiation.vo -theories/Wellfounded/Lexicographic_Product.vo -theories/Wellfounded/Transitive_Closure.vo -theories/Wellfounded/Union.vo -theories/Wellfounded/Wellfounded.vo -theories/Wellfounded/Well_Ordering.vo - -theories/ZArith/auxiliary.vo -theories/ZArith/BinInt.vo -theories/ZArith/Int.vo -theories/ZArith/Wf_Z.vo -theories/ZArith/Zabs.vo -theories/ZArith/ZArith_base.vo -theories/ZArith/ZArith_dec.vo -theories/ZArith/ZArith.vo -theories/ZArith/Zbinary.vo -theories/ZArith/Zbool.vo -theories/ZArith/Zcompare.vo -theories/ZArith/Zcomplements.vo -theories/ZArith/Zdiv.vo -theories/ZArith/Zeven.vo -theories/ZArith/Zgcd_alt.vo -theories/ZArith/Zhints.vo -theories/ZArith/Zlogarithm.vo -theories/ZArith/Zmax.vo -theories/ZArith/Zminmax.vo -theories/ZArith/Zmin.vo -theories/ZArith/Zmisc.vo -theories/ZArith/Znat.vo -theories/ZArith/Znumtheory.vo -theories/ZArith/ZOdiv_def.vo -theories/ZArith/ZOdiv.vo -theories/ZArith/Zorder.vo -theories/ZArith/Zpow_def.vo -theories/ZArith/Zpower.vo -theories/ZArith/Zpow_facts.vo -theories/ZArith/Zsqrt.vo -theories/ZArith/Zwf.vo - -plugins/dp/Dp.vo -plugins/field/LegacyField_Compl.vo -plugins/field/LegacyField_Tactic.vo -plugins/field/LegacyField_Theory.vo -plugins/field/LegacyField.vo -plugins/fourier/Fourier_util.vo -plugins/fourier/Fourier.vo -plugins/funind/Recdef.vo -plugins/groebner/GroebnerR.vo -plugins/groebner/GroebnerZ.vo -plugins/interface/CoqInterface.vo -#plugins/interface/CoqParser.vo (should not be compiled) -plugins/micromega/CheckerMaker.vo -plugins/micromega/EnvRing.vo -plugins/micromega/Env.vo -#plugins/micromega/MExtraction.vo (extraction of micromega.ml) -plugins/micromega/OrderedRing.vo -plugins/micromega/Psatz.vo -plugins/micromega/QMicromega.vo -plugins/micromega/Refl.vo -plugins/micromega/RingMicromega.vo -plugins/micromega/RMicromega.vo -plugins/micromega/Tauto.vo -plugins/micromega/VarMap.vo -plugins/micromega/ZCoeff.vo -plugins/micromega/ZMicromega.vo -plugins/omega/OmegaLemmas.vo -plugins/omega/OmegaPlugin.vo -plugins/omega/Omega.vo -plugins/omega/PreOmega.vo -plugins/quote/Quote.vo -plugins/ring/LegacyArithRing.vo -plugins/ring/LegacyNArithRing.vo -plugins/ring/LegacyRing_theory.vo -plugins/ring/LegacyRing.vo -plugins/ring/LegacyZArithRing.vo -plugins/ring/Ring_abstract.vo -plugins/ring/Ring_normalize.vo -plugins/ring/Setoid_ring_normalize.vo -plugins/ring/Setoid_ring_theory.vo -plugins/ring/Setoid_ring.vo -plugins/romega/ReflOmegaCore.vo -plugins/romega/ROmega.vo -plugins/rtauto/Bintree.vo -plugins/rtauto/Rtauto.vo -plugins/setoid_ring/ArithRing.vo -plugins/setoid_ring/BinList.vo -plugins/setoid_ring/Field_tac.vo -plugins/setoid_ring/Field_theory.vo -plugins/setoid_ring/Field.vo -plugins/setoid_ring/InitialRing.vo -plugins/setoid_ring/NArithRing.vo -plugins/setoid_ring/RealField.vo -plugins/setoid_ring/Ring_base.vo -plugins/setoid_ring/Ring_equiv.vo -plugins/setoid_ring/Ring_polynom.vo -plugins/setoid_ring/Ring_tac.vo -plugins/setoid_ring/Ring_theory.vo -plugins/setoid_ring/Ring.vo -plugins/setoid_ring/ZArithRing.vo -- cgit v1.2.3