diff options
| -rw-r--r-- | _tags | 75 | ||||
| -rwxr-xr-x | build | 32 | ||||
| -rw-r--r-- | configure.ml | 11 | ||||
| -rw-r--r-- | coq-win32.itarget | 2 | ||||
| -rw-r--r-- | coq.itarget | 8 | ||||
| -rw-r--r-- | dev/doc/ocamlbuild.txt | 30 | ||||
| -rw-r--r-- | myocamlbuild.ml | 482 | ||||
| -rw-r--r-- | plugins/plugins.itarget | 3 | ||||
| -rw-r--r-- | plugins/pluginsbyte.itarget | 21 | ||||
| -rw-r--r-- | plugins/pluginsdyn.itarget | 24 | ||||
| -rw-r--r-- | plugins/pluginsopt.itarget | 21 | ||||
| -rw-r--r-- | plugins/pluginsvo.itarget | 12 | ||||
| -rw-r--r-- | theories/theories.itarget | 25 |
13 files changed, 32 insertions, 714 deletions
diff --git a/_tags b/_tags deleted file mode 100644 index 9f77416a0..000000000 --- a/_tags +++ /dev/null @@ -1,75 +0,0 @@ - -## tags for binaries - -<tools/coqmktop.{native,byte}> : use_str, use_unix -<tools/coqc.{native,byte}> : use_str, use_unix -<tools/coqdep_boot.{native,byte}> : use_unix -<tools/coqdep.{native,byte}> : use_str, use_unix -<tools/coq_tex.{native,byte}> : use_str -<tools/coq_makefile.{native,byte}> : use_str, use_unix -<tools/coqdoc/main.{native,byte}> : use_str -<ide/coqide_main.{native,byte}> : use_str, use_unix, ide -<checker/main.{native,byte}> : use_str, use_unix, thread -<plugins/micromega/csdpcert.{native,byte}> : use_nums, use_unix -<tools/mkwinapp.{native,byte}> : use_unix -<tools/fake_ide.{native,byte}> : use_unix, use_str - -## tags for ide - -<ide/**/*.{ml,mli}>: ide - -## tags for grammar.cm* - -<grammar/grammar.{cma,cmxa}> : use_unix - -## tags for camlp4 files - -"parsing/g_constr.ml4": use_compat5 -"parsing/g_ltac.ml4": use_compat5 -"parsing/g_prim.ml4": use_compat5 -"parsing/g_proofs.ml4": use_compat5 -"parsing/g_tactic.ml4": use_compat5 -"parsing/g_vernac.ml4": use_compat5 -"parsing/g_xml.ml4": use_compat5 -"parsing/pcoq.ml4": use_compat5 -"parsing/g_obligations.ml4": use_grammar - -"grammar/argextend.ml4": use_compat5b -"grammar/tacextend.ml4": use_compat5b -"grammar/vernacextend.ml4": use_compat5b - -<tactics/*.ml4>: use_grammar - -<plugins/**/*.ml4>: use_grammar -"plugins/decl_mode/g_decl_mode.ml4": use_compat5 -"plugins/funind/g_indfun.ml4": use_compat5 - -## sub-directory inclusion - -# Note: "checker" is deliberately not included -# Note: same for "config" (we create a special coq_config.ml) - -"parsing": include -"ide": include -"ide/utils": include -"interp": include -"intf": include -"grammar": include -"kernel": include -"kernel/byterun": include -"lib": include -"library": include -"parsing": include -"plugins": include -"engine": include -"pretyping": include -"printing": include -"proofs": include -"stm": include -"tactics": include -"theories": include -"tools": include -"tools/coqdoc": include -"toplevel": include - -<plugins/**>: include diff --git a/build b/build deleted file mode 100755 index debf29cf4..000000000 --- a/build +++ /dev/null @@ -1,32 +0,0 @@ -#!/bin/sh - -FLAGS="-j 2" -OCAMLBUILD=ocamlbuild -MYCFG=myocamlbuild_config.ml - -export CAML_LD_LIBRARY_PATH=`pwd`/_build/kernel/byterun - -check_config() { - if [ ! -f $MYCFG ]; then echo "please run ./configure first"; exit 1; fi -} - -ocb() { $OCAMLBUILD $FLAGS $*; } - -rule() { - check_config - case $1 in - clean) ocb -clean && rm -rf bin/*;; - all) ocb coq.otarget;; - win32) ocb coq-win32.otarget;; - *) ocb $1;; - esac; -} - -if [ $# -eq 0 ]; then - rule all -else - while [ $# -gt 0 ]; do - rule $1; - shift - done -fi diff --git a/configure.ml b/configure.ml index ade43810b..1ea56d3ce 100644 --- a/configure.ml +++ b/configure.ml @@ -1003,7 +1003,7 @@ let write_dbg_wrapper f = let _ = write_dbg_wrapper "dev/ocamldebug-coq" -(** * Build the config/coq_config.ml file (+ link to myocamlbuild_config.ml) *) +(** * Build the config/coq_config.ml file *) let write_configml f = safe_remove f; @@ -1070,14 +1070,7 @@ let write_configml f = close_out o; Unix.chmod f 0o444 -let write_configml_my f f' = - write_configml f; - if os_type_win32 then - write_configml f' - else - (safe_remove f'; Unix.symlink f f') - -let _ = write_configml_my "config/coq_config.ml" "myocamlbuild_config.ml" +let _ = write_configml "config/coq_config.ml" (** * Build the config/Makefile file *) diff --git a/coq-win32.itarget b/coq-win32.itarget deleted file mode 100644 index 9e2c7a2b6..000000000 --- a/coq-win32.itarget +++ /dev/null @@ -1,2 +0,0 @@ -binariesopt -plugins/pluginsdyn.otarget diff --git a/coq.itarget b/coq.itarget deleted file mode 100644 index dd8b25905..000000000 --- a/coq.itarget +++ /dev/null @@ -1,8 +0,0 @@ -# NB: for the moment we start with bytecode compilation -# for early error detection in .ml -binariesbyte -plugins/pluginsbyte.otarget -binariesopt -plugins/pluginsopt.otarget -theories/theories.otarget -plugins/pluginsvo.otarget diff --git a/dev/doc/ocamlbuild.txt b/dev/doc/ocamlbuild.txt new file mode 100644 index 000000000..efedbc506 --- /dev/null +++ b/dev/doc/ocamlbuild.txt @@ -0,0 +1,30 @@ +Ocamlbuild & Coq +---------------- + +A quick note in case someone else gets interested someday in compiling +Coq via ocamlbuild : such an experimental build system has existed +in the past (more or less maintained from 2009 to 2013), in addition +to the official build system via gnu make. But this build via +ocamlbuild has been severly broken since early 2014 (and don't work +in 8.5, for instance). This experiment has attracted very limited +interest from other developers over the years, and has been quite +cumbersome to maintain, so it is now officially discontinued. +If you want to have a look at the files of this build system +(especially myocamlbuild.ml), you can fetch : + - my last effort at repairing this build system (up to coqtop.native) : + https://github.com/letouzey/coq-wip/tree/ocamlbuild-partial-repair + - coq official v8.5 branch (recent but broken) + - coq v8.4 branch(less up-to-date, but works). + +For the record, the three main drawbacks of this experiments were: + - recurrent issues with circularities reported by ocamlbuild + (even though make was happy) during the evolution of Coq sources + - no proper support of parallel build + - quite slow re-traversal of already built things +See the two corresponding bug reports on Mantis, or +https://github.com/ocaml/ocamlbuild/issues/52 + +As an interesting feature, I successfully used this to cross-compile +Coq 8.4 from linux to win32 via mingw. + +Pierre Letouzey, june 2016 diff --git a/myocamlbuild.ml b/myocamlbuild.ml deleted file mode 100644 index b81b280ff..000000000 --- a/myocamlbuild.ml +++ /dev/null @@ -1,482 +0,0 @@ -(** * Plugin for building Coq via Ocamlbuild *) - -open Ocamlbuild_plugin -open Ocamlbuild_pack -open Printf -open Scanf - -(** WARNING !! this is preliminary stuff. It should allows you to - build coq and its libraries if everything goes right. - Support for all the build rules and configuration options - is progressively added. Tested only on linux + ocaml 3.11 + - local + natdynlink for now. - - Usage: - ./configure -local -opt - ./build (which launches ocamlbuild coq.otarget) - - Then you can (hopefully) launch bin/coqtop, bin/coqide and so on. - Apart from the links in bin, every created files are in _build. - A "./build clean" should give you back a clean source tree - -*) - -(** F.A.Q about ocamlbuild: - -* P / Px ? - - Same, except that the second can be use to signal the main target - of a rule, in order to get a nicer log (otherwise the full command - is used as target name) - -*) - - - -(** Generic file reader, which produces a list of strings, one per line *) - -let read_file f = - 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 - - -(** 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 - -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 w32 = Coq_config.arch_is_win32 - -let w32pref = "i586-mingw32msvc" -let w32ocamlc = w32pref^"-ocamlc" -let w32ocamlopt = w32pref^"-ocamlopt" -let w32ocamlmklib = w32pref^"-ocamlmklib" -let w32res = w32pref^"-windres" -let w32lib = "/usr/"^w32pref^"/lib/" -let w32bin = "/usr/"^w32pref^"/bin/" -let w32ico = "ide/coq_icon.o" - -let _ = if w32 then begin - Options.ocamlopt := A w32ocamlopt; - Options.ocamlmklib := A w32ocamlmklib; -end - -let use_camlp5 = (Coq_config.camlp4 = "camlp5") - -let camlp4args = - if use_camlp5 then [A "pa_extend.cmo";A "q_MLast.cmo";A "pa_macro.cmo"] - else [] - -let ocaml = A Coq_config.ocaml -let camlp4o = S ((A Coq_config.camlp4o) :: camlp4args) -let camlp4incl = S[A"-I"; A Coq_config.camlp4lib] -let camlp4compat = Sh Coq_config.camlp4compat -let opt = (Coq_config.best = "opt") -let ide = Coq_config.has_coqide -let hasdynlink = Coq_config.has_natdynlink -let os5fix = (Coq_config.natdynlinkflag = "os5fixme") -let dep_dynlink = if hasdynlink then N else Sh"-natdynlink no" -let lablgtkincl = Sh Coq_config.coqideincl -let local = Coq_config.local -let cflags = S[A"-ccopt";A Coq_config.cflags] - -(** Do we want to inspect .ml generated from .ml4 ? *) -let readable_genml = false -let readable_flag = if readable_genml then A"pr_o.cmo" else N - -let _build = Options.build_dir - - -(** Abbreviations about files *) - -let core_libs = - ["lib/clib"; "lib/lib"; "kernel/kernel"; "library/library"; - "engine/engine"; "pretyping/pretyping"; "interp/interp"; "proofs/proofs"; - "parsing/parsing"; "printing/printing"; "tactics/tactics"; - "stm/stm"; "toplevel/toplevel"; "parsing/highparsing"; - "ltac/ltac"] -let core_cma = List.map (fun s -> s^".cma") core_libs -let core_cmxa = List.map (fun s -> s^".cmxa") core_libs -let core_mllib = List.map (fun s -> s^".mllib") core_libs - -let tolink = "tools/tolink.ml" - -let c_headers_base = - ["coq_fix_code.h";"coq_instruct.h"; "coq_memory.h"; - "coq_gc.h"; "coq_interp.h"; "coq_values.h"; - "coq_jumptbl.h"] -let c_headers = List.map ((^) "kernel/byterun/") c_headers_base - -let coqinstrs = "kernel/byterun/coq_instruct.h" -let coqjumps = "kernel/byterun/coq_jumptbl.h" -let copcodes = "kernel/copcodes.ml" - -let libcoqrun = "kernel/byterun/libcoqrun.a" - -let init_vo = "theories/Init/Prelude.vo" - -let nmake = "theories/Numbers/Natural/BigN/NMake_gen.v" -let nmakegen = "theories/Numbers/Natural/BigN/NMake_gen.ml" - -let adapt_name (pref,oldsuf,newsuf) f = - pref ^ (Filename.chop_suffix f oldsuf) ^ newsuf - -let get_names (oldsuf,newsuf) s = - let pref = Filename.dirname s ^ "/" in - List.map (adapt_name (pref,oldsuf,newsuf)) (string_list_of_file s) - -let get_vo_itargets f = - let vo_itargets = get_names (".otarget",".itarget") f in - List.flatten (List.map (get_names (".vo",".v")) vo_itargets) - -let theoriesv = get_vo_itargets "theories/theories.itarget" - -let pluginsv = get_vo_itargets "plugins/pluginsvo.itarget" - -let pluginsmllib = get_names (".cma",".mllib") "plugins/pluginsbyte.itarget" - -(** for correct execution of coqdep_boot, source files should have - been imported in _build (and NMake_gen.v should have been created). *) - -let coqdepdeps = theoriesv @ pluginsv @ pluginsmllib - -let coqtop = "toplevel/coqtop" -let coqide = "ide/coqide" -let coqdepboot = "tools/coqdep_boot" -let coqmktop = "tools/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 | Ide - -let all_binaries = - (if w32 then [ "mkwinapp", "tools/mkwinapp", Best ] else []) @ - [ "coqtop", coqtop, Both; - "coqide", "ide/coqide_main", Ide; - "coqmktop", coqmktop, Both; - "coqc", "tools/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; - "fake_ide", "tools/fake_ide", Best; - ] - - -let best_oext = if opt then ".native" else ".byte" -let best_ext = if opt then ".opt" else ".byte" -let best_iext = if ide = "opt" then ".opt" else ".byte" - -let coqtopbest = coqtop^best_oext -(* For inner needs, we rather use the bytecode versions of coqdep - and coqmktop: slightly slower but compile quickly, and ok with - w32 cross-compilation *) -let coqdep_boot = coqdepboot^".byte" -let coqmktop_boot = coqmktop^".byte" - -let binariesopt_deps = - let addext b = b ^ ".native" in - let rec deps = function - | [] -> [] - | (_,b,Ide)::l -> if ide="opt" then addext b :: deps l else deps l - | (_,b,_)::l -> if opt then addext b :: deps l else deps l - in deps all_binaries - -let binariesbyte_deps = - let addext b = b ^ ".byte" in - let rec deps = function - | [] -> [] - | (_,b,Ide)::l -> if ide<>"no" then addext b :: deps l else deps l - | (_,b,Both)::l -> addext b :: deps l - | (_,b,_)::l -> if not opt then addext b :: deps l else deps l - in deps all_binaries - -let ln_sf toward f = - Command.execute ~quiet:true (Cmd (S [A"ln";A"-sf";P toward;P f])) - -let rec make_bin_links = function - | [] -> () - | (b,ob,kind)::l -> - make_bin_links l; - let obd = "../"^ !_build^"/"^ob and bd = "bin/"^b in - match kind with - | Ide when ide <> "no" -> - ln_sf (obd^".byte") (bd^".byte"); - if ide = "opt" then ln_sf (obd^".native") (bd^".opt"); - ln_sf (b^best_iext) bd - | Ide (* when ide = "no" *) -> () - | Both -> - ln_sf (obd^".byte") (bd^".byte"); - if opt then ln_sf (obd^".native") (bd^".opt"); - ln_sf (b^best_ext) bd - | Best -> ln_sf (obd^best_oext) bd - | BestInPlace -> ln_sf (b^best_oext) (!_build^"/"^ob) - -let incl f = Ocaml_utils.ocaml_include_flags f - -let cmd cl = (fun _ _ -> (Cmd (S cl))) - -let initial_actions () = begin - (** We "pre-create" a few subdirs in _build *) - Shell.mkdir_p (!_build^"/dev"); - Shell.mkdir_p (!_build^"/bin"); - Shell.mkdir_p (!_build^"/plugins/micromega"); - make_bin_links all_binaries; -end - -let extra_rules () = begin - -(** Virtual target for building all binaries *) - - rule "binariesopt" ~stamp:"binariesopt" ~deps:binariesopt_deps (fun _ _ -> Nop); - rule "binariesbyte" ~stamp:"binariesbyte" ~deps:binariesbyte_deps (fun _ _ -> Nop); - rule "binaries" ~stamp:"binaries" ~deps:["binariesbyte";"binariesopt"] (fun _ _ -> Nop); - -(** We create a special coq_config which mentions _build *) - - rule "coq_config.ml" ~prod:"coq_config.ml" ~dep:"config/coq_config.ml" - (fun _ _ -> - if w32 then cp "config/coq_config.ml" "coq_config.ml" else - let lines = read_file "config/coq_config.ml" in - let lines = List.map (fun s -> s^"\n") lines in - let line0 = "\n(* Adapted variables for ocamlbuild *)\n" in - (* TODO : line2 isn't completely accurate with respect to ./configure: - the case of -local -vmbyteflags foo isn't supported *) - let line1 = - "let vmbyteflags = [\"-dllib\";\"-lcoqrun\"]\n" - in - Echo (lines @ (if local then [line0;line1] else []), - "coq_config.ml")); - -(** Camlp4 extensions *) - - rule ".ml4.ml" ~dep:"%.ml4" ~prod:"%.ml" - (fun env _ -> - let ml4 = env "%.ml4" and ml = env "%.ml" in - Cmd (S[camlp4o;T(tags_of_pathname ml4 ++ "p4mod");readable_flag; - T(tags_of_pathname ml4 ++ "p4option"); camlp4compat; - A"-o"; Px ml; A"-impl"; P ml4])); - - flag_and_dep ["p4mod"; "use_grammar"] (P "grammar/grammar.cma"); - - flag_and_dep ["p4mod"; "use_compat5"] (P "tools/compat5.cmo"); - flag_and_dep ["p4mod"; "use_compat5b"] (P "tools/compat5b.cmo"); - - if w32 then begin - flag ["p4mod"] (A "-DWIN32"); - dep ["ocaml"; "link"; "ide"] ["ide/ide_win32_stubs.o"]; - end; - - if not use_camlp5 then begin - let mlp_cmo s = - let src=s^".mlp" and dst=s^".cmo" in - rule (src^".cmo") ~dep:src ~prod:dst ~insert:`top - (fun env _ -> - Cmd (S [!Options.ocamlc; A"-c"; A"-pp"; - Quote (S [camlp4o;A"-impl"]); camlp4incl; A"-impl"; P src])) - in - mlp_cmo "tools/compat5"; - mlp_cmo "tools/compat5b"; - end; - -(** All caml files are compiled with +camlp4/5 - and ide files need +lablgtk2 *) - - flag ["compile"; "ocaml"] (S [A"-thread";A"-rectypes"; camlp4incl]); - flag ["link"; "ocaml"] (S [A"-rectypes"; camlp4incl]); - flag ["ocaml"; "ide"; "compile"] lablgtkincl; - flag ["ocaml"; "ide"; "link"] lablgtkincl; - flag ["ocaml"; "ide"; "link"; "byte"] - (S [A"lablgtk.cma"; A"lablgtksourceview2.cma"]); - flag ["ocaml"; "ide"; "link"; "native"] - (S [A"lablgtk.cmxa"; A"lablgtksourceview2.cmxa"]); - -(** C code for the VM *) - - dep ["compile"; "c"] c_headers; - flag ["compile"; "c"] cflags; - dep ["ocaml"; "use_libcoqrun"; "compile"] [libcoqrun]; - dep ["ocaml"; "use_libcoqrun"; "link"; "native"] [libcoqrun]; - flag ["ocaml"; "use_libcoqrun"; "link"; "byte"] (Sh Coq_config.vmbyteflags); - - (* we need to use a different ocamlc. For now we copy the rule *) - if w32 then - rule ".c.o" ~deps:("%.c"::c_headers) ~prod:"%.o" ~insert:`top - (fun env _ -> - let c = env "%.c" in - let o = env "%.o" in - Seq [Cmd (S [P w32ocamlc;cflags;A"-c";Px c]); - mv (Filename.basename o) o]); - -(** VM: Generation of coq_jumbtbl.h and copcodes.ml from coq_instruct.h *) - - rule "coqinstrs" ~dep:coqinstrs ~prods:[coqjumps;copcodes] - (fun _ _ -> - let jmps = ref [] and ops = ref [] and i = ref 0 in - let add_instr instr comma = - if instr = "" then failwith "Empty" else begin - jmps:=sprintf "&&coq_lbl_%s%s \n" instr comma :: !jmps; - ops:=sprintf "let op%s = %d\n" instr !i :: !ops; - incr i - end - in - (** we recognize comma-separated uppercase instruction names *) - let parse_line s = - let b = Scanning.from_string s in - try while true do bscanf b " %[A-Z0-9_]%[,]" add_instr done - with _ -> () - in - List.iter parse_line (read_file coqinstrs); - Seq [Echo (List.rev !jmps, coqjumps); - Echo (List.rev !ops, copcodes)]); - -(** Generation of tolink.ml *) - - rule tolink ~deps:core_mllib ~prod:tolink - (fun _ _ -> - let cat s = String.concat " " (string_list_of_file s) in - let core_mods = String.concat " " (List.map cat core_mllib) in - let core_cmas = String.concat " " core_cma in - Echo (["let copts = \"-cclib -lcoqrun\"\n"; - "let core_libs = \""^core_cmas^"\"\n"; - "let core_objs = \""^core_mods^"\"\n"], - tolink)); - -(** For windows, building coff object file from a .rc (for the icon) *) - - if w32 then rule ".rc.o" ~deps:["%.rc";"ide/coq.ico"] ~prod:"%.o" - (fun env _ -> - let rc = env "%.rc" and o = env "%.o" in - Cmd (S [P w32res;A "--input-format";A "rc";A "--input";P rc; - A "--output-format";A "coff";A "--output"; Px o])); - -(** The windows version of Coqide is now a console-free win32 app, - which moreover contains the Coq icon. If necessary, the mkwinapp - tool can be used later to restore or suppress the console of Coqide. *) - - if w32 then dep ["link"; "ocaml"; "program"; "ide"] [w32ico]; - - if w32 then flag ["link"; "ocaml"; "program"; "ide"] - (S [A "-ccopt"; A "-link -Wl,-subsystem,windows"; P w32ico]); - -(** Coqtop *) - - let () = - let fo = coqtop^".native" and fb = coqtop^".byte" in - let depsall = (if w32 then [w32ico] else [])@[coqmktop_boot;libcoqrun] in - let depso = core_cmxa in - let depsb = core_cma in - let w32flag = - if not w32 then N else S ([A"-camlbin";A w32bin;A "-ccopt";P w32ico]) - in - if opt then rule fo ~prod:fo ~deps:(depsall@depso) ~insert:`top - (cmd [P coqmktop_boot;w32flag;A"-boot";A"-opt";incl fo;A"-thread";camlp4incl;A"-o";Px fo]); - rule fb ~prod:fb ~deps:(depsall@depsb) ~insert:`top - (cmd [P coqmktop_boot;w32flag;A"-boot";A"-top";incl fb;A"-thread";camlp4incl;A"-o";Px fb]); - in - -(** Coq files dependencies *) - - rule "coqdepready" ~stamp:"coqdepready" ~deps:coqdepdeps (fun _ _ -> Nop); - - rule ".v.d" ~prod:"%.v.depends" ~deps:["%.v";coqdep_boot;"coqdepready"] - (fun env _ -> - let v = env "%.v" and vd = env "%.v.depends" in - (** NB: this relies on all .v files being already in _build. *) - Cmd (S [P coqdep_boot;dep_dynlink;P v;Sh">";Px vd])); - -(** Coq files compilation *) - - let coq_build_dep f build = - (** NB: this relies on coqdep producing a single Makefile line - for one .v file, with some specific shape "f.vo ...: f.v deps.vo ..." *) - let src = f^".v" in - let depends = f^".v.depends" in - let rec get_deps keep = function - | [] -> [] - | d::deps when d = src -> get_deps keep deps - | d::deps when keep -> [d] :: get_deps keep deps - | d::deps -> get_deps (String.contains d ':') deps - in - let d = get_deps false (string_list_of_file depends) in - List.iter Outcome.ignore_good (build d) - - in - - let coq_v_rule d init = - let bootflag = if init then A"-noinit" else N in - let gendep = if init then coqtopbest else init_vo in - rule (d^".v.vo") - ~prods:[d^"%.vo";d^"%.glob"] ~deps:[gendep;d^"%.v";d^"%.v.depends"] - (fun env build -> - let f = env (d^"%") in - coq_build_dep f build; - Cmd (S [P coqtopbest;A"-boot";bootflag;A"-compile";Px f])) - in - coq_v_rule "theories/Init/" true; - coq_v_rule "" false; - -(** Generation of _plugin_mod.ml files *) - - rule "_mod.ml" ~prod:"%_plugin_mod.ml" ~dep:"%_plugin.mllib" - (fun env _ -> - let line s = "let _ = Mltop.add_known_module \""^s^"\"\n" in - let mods = - string_list_of_file (env "%_plugin.mllib") @ - [Filename.basename (env "%_plugin")] - in - Echo (List.map line mods, env "%_plugin_mod.ml")); - -(** Rule for native dynlinkable plugins *) - - rule ".cmxa.cmxs" ~prod:"%.cmxs" ~dep:"%.cmxa" - (fun env _ -> - let cmxs = Px (env "%.cmxs") and cmxa = P (env "%.cmxa") in - if os5fix then - Cmd (S [A"../dev/ocamlopt_shared_os5fix.sh"; !Options.ocamlopt; cmxs]) - else - Cmd (S [!Options.ocamlopt;A"-linkall";A"-shared";A"-o";cmxs;cmxa])); - -(** Generation of NMake.v from NMake_gen.ml *) - - rule "NMake" ~prod:nmake ~dep:nmakegen - (cmd [ocaml;P nmakegen;Sh ">";Px nmake]); - -end - -(** Registration of our rules (after the standard ones) *) - -let _ = dispatch begin function - | After_rules -> initial_actions (); extra_rules () - | _ -> () -end - -(** TODO / Remarques: - - * Apres un premier build, le second prend du temps, meme cached: - 1 min 25 pour les 2662 targets en cache. Etonnement, refaire - coqtop.byte ne prend que ~4s, au lieu des ~40s pour coqtop.opt. - A comprendre ... - - * Parallelisation: vraiment pas top - -*) diff --git a/plugins/plugins.itarget b/plugins/plugins.itarget deleted file mode 100644 index 56aa42b06..000000000 --- a/plugins/plugins.itarget +++ /dev/null @@ -1,3 +0,0 @@ -pluginsopt.otarget -pluginsbyte.otarget -pluginsvo.otarget
\ No newline at end of file diff --git a/plugins/pluginsbyte.itarget b/plugins/pluginsbyte.itarget deleted file mode 100644 index d8752f8b8..000000000 --- a/plugins/pluginsbyte.itarget +++ /dev/null @@ -1,21 +0,0 @@ -btauto/btauto_plugin.cma -setoid_ring/newring_plugin.cma -extraction/extraction_plugin.cma -decl_mode/decl_mode_plugin.cma -firstorder/ground_plugin.cma -rtauto/rtauto_plugin.cma -fourier/fourier_plugin.cma -romega/romega_plugin.cma -omega/omega_plugin.cma -micromega/micromega_plugin.cma -cc/cc_plugin.cma -nsatz/nsatz_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 -derive/derive_plugin.cma
\ No newline at end of file diff --git a/plugins/pluginsdyn.itarget b/plugins/pluginsdyn.itarget deleted file mode 100644 index 220e5182d..000000000 --- a/plugins/pluginsdyn.itarget +++ /dev/null @@ -1,24 +0,0 @@ -btauto/btauto_plugin.cmxs -field/field_plugin.cmxs -setoid_ring/newring_plugin.cmxs -extraction/extraction_plugin.cmxs -decl_mode/decl_mode_plugin.cmxs -firstorder/ground_plugin.cmxs -rtauto/rtauto_plugin.cmxs -fourier/fourier_plugin.cmxs -romega/romega_plugin.cmxs -omega/omega_plugin.cmxs -micromega/micromega_plugin.cmxs -subtac/subtac_plugin.cmxs -ring/ring_plugin.cmxs -cc/cc_plugin.cmxs -nsatz/nsatz_plugin.cmxs -funind/recdef_plugin.cmxs -syntax/ascii_syntax_plugin.cmxs -syntax/nat_syntax_plugin.cmxs -syntax/numbers_syntax_plugin.cmxs -syntax/r_syntax_plugin.cmxs -syntax/string_syntax_plugin.cmxs -syntax/z_syntax_plugin.cmxs -quote/quote_plugin.cmxs -derive/derive_plugin.cmxs diff --git a/plugins/pluginsopt.itarget b/plugins/pluginsopt.itarget deleted file mode 100644 index 04a1e711c..000000000 --- a/plugins/pluginsopt.itarget +++ /dev/null @@ -1,21 +0,0 @@ -btauto/btauto_plugin.cmxa -setoid_ring/newring_plugin.cmxa -extraction/extraction_plugin.cmxa -decl_mode/decl_mode_plugin.cmxa -firstorder/ground_plugin.cmxa -rtauto/rtauto_plugin.cmxa -fourier/fourier_plugin.cmxa -romega/romega_plugin.cmxa -omega/omega_plugin.cmxa -micromega/micromega_plugin.cmxa -cc/cc_plugin.cmxa -nsatz/nsatz_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 -derive/derive_plugin.cmxa diff --git a/plugins/pluginsvo.itarget b/plugins/pluginsvo.itarget deleted file mode 100644 index a59bf29c9..000000000 --- a/plugins/pluginsvo.itarget +++ /dev/null @@ -1,12 +0,0 @@ -btauto/vo.otarget -fourier/vo.otarget -funind/vo.otarget -nsatz/vo.otarget -micromega/vo.otarget -omega/vo.otarget -quote/vo.otarget -romega/vo.otarget -rtauto/vo.otarget -setoid_ring/vo.otarget -extraction/vo.otarget -derive/vo.otarget
\ No newline at end of file diff --git a/theories/theories.itarget b/theories/theories.itarget deleted file mode 100644 index aacab2d97..000000000 --- a/theories/theories.itarget +++ /dev/null @@ -1,25 +0,0 @@ -Arith/vo.otarget -Bool/vo.otarget -Classes/vo.otarget -Compat/vo.otarget -FSets/vo.otarget -MSets/vo.otarget -Structures/vo.otarget -Init/vo.otarget -Lists/vo.otarget -Vectors/vo.otarget -Logic/vo.otarget -PArith/vo.otarget -NArith/vo.otarget -Numbers/vo.otarget -Program/vo.otarget -QArith/vo.otarget -Reals/vo.otarget -Relations/vo.otarget -Setoids/vo.otarget -Sets/vo.otarget -Sorting/vo.otarget -Strings/vo.otarget -Unicode/vo.otarget -Wellfounded/vo.otarget -ZArith/vo.otarget |