Skip to content


Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Fetching contributors…

Cannot retrieve contributors at this time

494 lines (389 sloc) 17.006 kb
(** * 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.
./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 indirectly : we symlink it to, which is linked with this *)
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;
let w32 = (Coq_config.arch = "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;
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 = ( = "opt")
let ide = Coq_config.has_coqide
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 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
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/lib"; "kernel/kernel"; "library/library";
"pretyping/pretyping"; "interp/interp"; "proofs/proofs";
"parsing/parsing"; "tactics/tactics"; "toplevel/toplevel";
"parsing/highparsing"; "tactics/hightactics"]
let core_cma = (fun s -> s^".cma") core_libs
let core_cmxa = (fun s -> s^".cmxa") core_libs
let core_mllib = (fun s -> s^".mllib") core_libs
let ide_cma = "ide/ide.cma"
let ide_cmxa = "ide/ide.cmxa"
let ide_mllib = "ide/ide.mllib"
let tolink = "scripts/"
let c_headers_base =
["coq_fix_code.h";"coq_instruct.h"; "coq_memory.h"; "int64_emul.h";
"coq_gc.h"; "coq_interp.h"; "coq_values.h"; "int64_native.h";
let c_headers = ((^) "kernel/byterun/") c_headers_base
let coqinstrs = "kernel/byterun/coq_instruct.h"
let coqjumps = "kernel/byterun/coq_jumptbl.h"
let copcodes = "kernel/"
let libcoqrun = "kernel/byterun/libcoqrun.a"
let grammar = "parsing/grammar.cma"
let qconstr = "parsing/q_constr.cmo"
let refutpat = "lib/refutpat.cmo"
let initialcoq = "states/initial.coq"
let init_vo = ["theories/Init/Prelude.vo";"theories/Init/Logic_Type.vo"]
let makeinitial = "states/MakeInitial.v"
let nmake = "theories/Numbers/Natural/BigN/NMake_gen.v"
let nmakegen = "theories/Numbers/Natural/BigN/"
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 (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 ( (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 = "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 | Ide
let all_binaries =
(if w32 then [ "mkwinapp", "tools/mkwinapp", Best ] else []) @
[ "coqtop", coqtop, Both;
"coqide", coqide, Ide;
"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 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
let coqdepbest = coqdepboot^(if w32 then ".byte" else best_oext)
let coqmktopbest = coqmktop^(if w32 then ".byte" else best_oext)
let binaries_deps =
let rec deps = function
| [] -> []
| (_,bin,Ide)::l ->
(if ide = "opt" then [bin^".native"] else []) @
(if ide <> "no" then [bin^".byte"] else []) @ deps l
| (_,bin,Both)::l when opt ->
(bin^".native") :: (bin^".byte") :: deps l
| (_,bin,_)::l -> (bin^best_oext) :: deps l
in deps all_binaries
let binariesopt_deps =
List.filter (fun s -> Filename.check_suffix s ".native") binaries_deps
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;
let extra_rules () = begin
(** Virtual target for building all binaries *)
rule "binaries" ~stamp:"binaries" ~deps:binaries_deps (fun _ _ -> Nop);
rule "binariesopt" ~stamp:"binariesopt" ~deps:binariesopt_deps (fun _ _ -> Nop);
(** We create a special coq_config which mentions _build *)
rule "" ~prod:"" ~dep:"config/"
(fun _ _ ->
if w32 then cp "config/" "" else
let lines = read_file "config/" in
let lines = (fun s -> s^"\n") lines in
let srcbuild = Filename.concat coqsrc !_build in
let line0 = "\n(* Adapted variables for ocamlbuild *)\n" in
let line1 = "let coqsrc = \""^srcbuild^"\"\n" in
let line2 = "let coqlib = \""^srcbuild^"\"\n" in
(* TODO : line3 isn't completely accurate with respect to ./configure:
the case of -local -coqrunbyteflags foo isn't supported *)
let line3 =
"let coqrunbyteflags = \"-dllib -lcoqrun -dllpath '"
Echo (lines @ [line0;line1] @ (if local then [line2;line3] else []),
(** Camlp4 extensions *)
rule "" ~dep:"%.ml4" ~prod:""
(fun env _ ->
let ml4 = env "%.ml4" and ml = env "" 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 ["is_ml4"; "p4mod"; "use_macro"] (A"pa_macro.cmo");
flag ["is_ml4"; "p4mod"; "use_extend"] (A"pa_extend.cmo");
flag ["is_ml4"; "p4mod"; "use_MLast"] (A"q_MLast.cmo");
flag_and_dep ["is_ml4"; "p4mod"; "use_grammar"] (P grammar);
flag_and_dep ["is_ml4"; "p4mod"; "use_constr"] (P qconstr);
flag_and_dep ["is_ml4"; "p4mod"; "use_refutpat"] (P refutpat);
(** Special case of toplevel/mltop.ml4:
- will be the old mltop.optml and be used to obtain mltop.cmx
- we add a special mltop.ml4 --> mltop.cmo rule, before all the others
flag ["is_mltop"; "p4option"] flag_dynlink;
(*TODO: this is rather ugly for a simple file, we should try to
benefit more from predefined rules *)
let mltop = "toplevel/mltop" in
let ml4 = mltop^".ml4" and mlo = mltop^".cmo" and
ml = mltop^".ml" and mld = mltop^".ml.depends"
rule "mltop_byte" ~deps:[ml4;mld] ~prod:mlo ~insert:`top
(fun env build ->
Ocaml_compiler.prepare_compile build ml;
Cmd (S [!Options.ocamlc; A"-c"; A"-pp";
Quote (S [camlp4o; T(tags_of_pathname ml4 ++ "p4mod");
A"-rectypes"; camlp4incl; incl ml4; A"-impl"; P ml4]));
(** All caml files are compiled with -rectypes and +camlp4/5
and ide files need +lablgtk2 *)
flag ["compile"; "ocaml"] (S [A"-rectypes"; camlp4incl]);
flag ["link"; "ocaml"] (S [A"-rectypes"; camlp4incl]);
flag ["compile"; "ocaml"; "ide"] lablgtkincl;
flag ["link"; "ocaml"; "ide"] lablgtkincl;
(** Extra libraries *)
ocaml_lib ~extern:true "gramlib";
(** C code for the VM *)
dep ["compile"; "c"] c_headers;
flag ["compile"; "c"] cflags;
dep ["link"; "ocaml"; "use_libcoqrun"] [libcoqrun];
(* 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 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
(** 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 _ -> ()
List.iter parse_line (read_file coqinstrs);
Seq [Echo (List.rev !jmps, coqjumps);
Echo (List.rev !ops, copcodes)]);
(** Generation of *)
rule tolink ~deps:(ide_mllib::core_mllib) ~prod:tolink
(fun _ _ ->
let cat s = String.concat " " (string_list_of_file s) in
let core_mods = String.concat " " ( cat core_mllib) in
let ide_mods = cat ide_mllib in
let core_cmas = String.concat " " core_cma in
Echo (["let copts = \"-cclib -lcoqrun\"\n";
"let core_libs = \"coq_config.cmo "^core_cmas^"\"\n";
"let core_objs = \"Coq_config "^core_mods^"\"\n";
"let ide = \""^ide_mods^"\"\n"],
(** 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]));
(** Coqtop and coqide *)
let mktop_rule f is_ide =
let fo = f^".native" and fb = f^".byte" in
let ideflag = if is_ide then A"-ide" else N in
let depsall = [coqmktopbest;libcoqrun] in
let depsall = if w32 then w32ico::depsall else depsall in
let depso = "coq_config.cmx" :: core_cmxa in
let depsb = "coq_config.cmo" :: core_cma in
let depideo = if is_ide then [ide_cmxa] else [] in
let depideb = if is_ide then [ide_cma] else [] in
let w32ideflag =
(* Uncomment the following line to make coqide a console-free win32 app.
For the moment we don't, some issue remain to be investigated.
In the meantime, coqide can be made console-free a posteriori via
the mkwinapp tool. *)
(*if is_ide then [A"-ccopt";A"\"-link -Wl,-subsystem,windows\""] else*) [] in
let w32flag =
if not w32 then N
else S ([A"-camlbin";A w32bin;A "-ccopt";P w32ico]@w32ideflag)
if opt then rule fo ~prod:fo ~deps:(depsall@depso@depideo) ~insert:`top
(cmd [P coqmktopbest;w32flag;A"-boot";A"-opt";ideflag;incl fo;A"-o";Px fo]);
rule fb ~prod:fb ~deps:(depsall@depsb@depideb) ~insert:`top
(cmd [P coqmktopbest;w32flag;A"-boot";A"-top";ideflag;incl fb;A"-o";Px fb]);
mktop_rule coqtop false;
mktop_rule coqide true;
(** Coq files dependencies *)
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. *)
Cmd (S [P coqdepbest;dep_dynlink;A"-slash";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 : *)
match string_list_of_file (f^".v.depends") with
| vo::vg::v::deps when vo=f^".vo" && vg=f^".glob:" && v=f^".v" ->
let d = (fun x -> [x]) deps in
List.iter Outcome.ignore_good (build d)
| _ -> failwith ("Something wrong with dependencies of "^f^".v")
let coq_v_rule d init =
let bootflag = if init then A"-nois" else N in
let gendep = if init then coqtopbest else initialcoq 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]))
coq_v_rule "theories/Init/" true;
coq_v_rule "" false;
(** Initial state *)
rule "initial.coq" ~prod:initialcoq ~deps:(makeinitial::init_vo)
(cmd [P coqtopbest;A"-boot";A"-batch";A"-nois";A"-notop";A"-silent";
A"-l";P makeinitial; A"-outputstate";Px initialcoq]);
(** Generation of files *)
rule "" ~prod:"" ~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")]
Echo ( line mods, env ""));
(** 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/"; !Options.ocamlopt; cmxs])
Cmd (S [!Options.ocamlopt;A"-linkall";A"-shared";A"-o";cmxs;cmxa]));
(** Generation of NMake.v from *)
rule "NMake" ~prod:nmake ~dep:nmakegen
(cmd [ocaml;P nmakegen;Sh ">";Px nmake]);
(** Registration of our rules (after the standard ones) *)
let _ = dispatch begin function
| After_rules -> initial_actions (); extra_rules ()
| _ -> ()
(** 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
Jump to Line
Something went wrong with that request. Please try again.