aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-03-24 18:21:07 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-03-24 18:21:07 +0000
commit6a14070e4666cc8c0457b03c81ea99a9a6c4b833 (patch)
tree82a30290cec8006671fb933dc008ce96c4d9e891
parente0bd95f7c3e0304506d62a900ae26c58ec3d4f38 (diff)
ocamlbuild improvements + minor makefile fix
* a small shell script ./build to drive ocamlbuild * rules for all the binaries (apart from coqide and coqchk) * use of ocamlbuild's Echo instead of using shell + sed + awk for generated files * Makefile: remove unused STAGE1_CMO and add bin/coqdep_boot to the list of things to "clean" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12012 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--Makefile.common3
-rw-r--r--_tags7
-rwxr-xr-xbuild26
-rw-r--r--coq.itarget16
-rw-r--r--kernel/byterun/coq_instruct.h4
-rw-r--r--myocamlbuild.ml281
6 files changed, 227 insertions, 110 deletions
diff --git a/Makefile.common b/Makefile.common
index 8a258fb8c..e61a4e28a 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -87,7 +87,7 @@ COQTEX:=bin/coq-tex$(EXE)
COQWC:=bin/coqwc$(EXE)
COQDOC:=bin/coqdoc$(EXE)
-TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQWC) $(COQDOC)
+TOOLS:=$(COQDEP) $(COQDEPBOOT) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQWC) $(COQDOC)
###########################################################################
# Documentation
@@ -619,7 +619,6 @@ CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.cmxs %.dep.ps %.dot
## Enumeration of targets that require being done at stage1
STAGE1_TARGETS:= $(STAGE1) $(COQDEPBOOT) \
- $(filter-out parsing/q_constr.cmo,$(STAGE1_CMO)) \
$(GENFILES) \
source-doc revision toplevel/mltop.byteml toplevel/mltop.optml \
$(STAGE1_ML4:.ml4=.ml4-preprocessed) %.o
diff --git a/_tags b/_tags
index 7e8db8dd6..76a7da8a0 100644
--- a/_tags
+++ b/_tags
@@ -2,6 +2,12 @@
## tags for binaries
<scripts/coqmktop.{native,byte}> : use_str, use_unix, use_gramlib
+<scripts/coqc.{native,byte}> : use_unix, use_gramlib
+<tools/coqdep_boot.{native,byte}> : use_unix
+<tools/coqdep.{native,byte}> : use_unix, use_gramlib
+<tools/coq_tex.{native,byte}> : use_str
+<tools/coq_makefile.{native,byte}> : use_str
+<tools/coqdoc/main.{native,byte}> : use_str
## tags for camlp4 files
@@ -55,5 +61,6 @@
"tactics": include
"theories": include
"tools": include
+"tools/coqdoc": include
"toplevel": include
diff --git a/build b/build
new file mode 100755
index 000000000..4552d5a43
--- /dev/null
+++ b/build
@@ -0,0 +1,26 @@
+#!/bin/sh
+
+FLAGS=
+OCAMLBUILD=ocamlbuild
+
+ocb()
+{
+ $OCAMLBUILD $FLAGS $*
+}
+
+rule() {
+ case $1 in
+ clean) ocb -clean && rm -rf bin/*;;
+ all) ocb coq.otarget;;
+ *) ocb $1;;
+ esac;
+}
+
+if [ $# -eq 0 ]; then
+ rule all
+else
+ while [ $# -gt 0 ]; do
+ rule $1;
+ shift
+ done
+fi
diff --git a/coq.itarget b/coq.itarget
index 4845e1cdc..421082a3a 100644
--- a/coq.itarget
+++ b/coq.itarget
@@ -1,5 +1,11 @@
-bin/.foo
-scripts/coqmktop.byte
-scripts/coqmktop.native
-bin/coqtop.opt
-bin/coqtop.byte \ No newline at end of file
+bin/coqmktop
+bin/coqtop
+bin/coqc
+bin/coqdep
+bin/coqwc
+bin/coq-tex
+bin/coq_makefile
+bin/gallina
+bin/coqdoc
+# for the moment:
+bin/coqdep_boot \ No newline at end of file
diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h
index 8a45e9739..e224a1080 100644
--- a/kernel/byterun/coq_instruct.h
+++ b/kernel/byterun/coq_instruct.h
@@ -11,6 +11,10 @@
#ifndef _COQ_INSTRUCT_
#define _COQ_INSTRUCT_
+/* Nota: this list of instructions is parsed to produce derived files */
+/* coq_jumptbl.h and copcodes.ml. Instructions should be uppercase */
+/* and alone on lines starting by two spaces. */
+
enum instructions {
ACC0, ACC1, ACC2, ACC3, ACC4, ACC5, ACC6, ACC7, ACC,
PUSH,
diff --git a/myocamlbuild.ml b/myocamlbuild.ml
index b518c50d0..17dfcdff1 100644
--- a/myocamlbuild.ml
+++ b/myocamlbuild.ml
@@ -3,6 +3,7 @@
open Ocamlbuild_plugin
open Ocamlbuild_pack
open Printf
+open Scanf
(** WARNING !! this is preliminary stuff, able only to build
coqtop.opt and coqtop.byte, and only in a precise environment
@@ -11,48 +12,50 @@ open Printf
Support for other rules and other configurations will be
added later...
- Usage:
-
- ocamlbuild coq.otarget
+ Usage: ./build (which launches ocamlbuild coq.itarget)
Then you can (hopefully) launch coq (with no input state) via:
- _build/bin/coqtop.opt -nois -coqlib .
+ bin/coqtop.opt -nois -coqlib .
or
- CAML_LD_LIBRARY_PATH=_build/kernel/byterun _build/bin/coqtop.byte -nois -coqlib .
+ export CAML_LD_LIBRARY_PATH=_build/kernel/byterun
+ bin/coqtop.byte -nois -coqlib .
+
+ Apart from binaries in bin/, every created files are in _build.
+ A "./build clean" should give you back a clean source tree
TODO: understand how to create the right symlinks towards _build ...
*)
+(** 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 NAME=value, comments start by # *)
+(** 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 ic = open_in f in
- let vars = ref [] in
- begin try while true do
- let l = input_line ic in
- if l <> "" && l.[0] <> '#' && l.[0] <> ' ' then
- try
- let i = String.index l '=' in
- let var = String.sub l 0 i
- and def = if i+1 >= String.length l then "" else
- String.sub l (i+1) (String.length l - i - 1)
- in
- let def = if String.length def >= 2 &&
- def.[0]='\"' && def.[String.length def - 1] = '\"'
- then String.sub def 1 (String.length def - 2) else def
- in
- vars:=(var,def)::!vars
- with Not_found -> ()
- done with End_of_file -> () end;
- close_in ic;
- !vars
+ 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 env_vars =
let f = "config/Makefile" in
@@ -63,20 +66,28 @@ let get_env s =
with Not_found -> (eprintf "Unknown environment variable %s\n" s; exit 1)
+
(** Configuration *)
let _ = Options.ocamlc := A(get_env "OCAMLC")
-let camlp4o = get_env "CAMLP4O"
-let camlp4lib = get_env "MYCAMLP4LIB"
-let camlp4compat = get_env "CAMLP4COMPAT"
+let camlp4o = A(get_env "CAMLP4O")
+let camlp4lib = S[A"-I"; A(get_env "MYCAMLP4LIB")]
+let camlp4compat = Sh(get_env "CAMLP4COMPAT")
+let opt = (get_env "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" = "true")
-let flag_dynlink = if hasdynlink then "-DHasDynLink" else ""
+let flag_dynlink = if hasdynlink then A"-DHasDynLink" else N
(** 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
+
+
+(** Abbreviations about files *)
+
let core_libs =
["lib/lib"; "kernel/kernel"; "library/library";
"pretyping/pretyping"; "interp/interp"; "proofs/proofs";
@@ -86,31 +97,88 @@ 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 ide_mllib = "ide/ide.mllib"
+
+let tolink = "scripts/tolink.ml"
+let coqconfig = "config/coq_config"
+
+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";
+ "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 grammar = "parsing/grammar.cma"
+let qconstr = "parsing/q_constr.cmo"
+
+let coqtop = "bin/coqtop"
+let coqmktop = "bin/coqmktop"
+let coqdep_boot = "bin/coqdep_boot"
+let coqdep = "bin/coqdep"
+let coqdoc = "bin/coqdoc"
+let coqwc = "bin/coqwc"
+let coqtex = "bin/coq-tex"
+let coqmakefile = "bin/coq_makefile"
+let gallina = "bin/gallina"
+
+
+
+(** A few common rules *)
+
+let copy_rule src dst =
+ rule (src^"_"^dst) ~dep:src ~prod:dst (fun _ _ -> cp src dst)
+
+let copy_bin srcd radix =
+ let src = srcd^radix and dst = "bin/"^radix in
+ copy_rule (src^".byte") (dst^".byte");
+ if opt then copy_rule (src^".native") (dst^".opt")
+
+let copy_bin_alias srcd radix =
+ let f = "bin/"^radix in
+ let fo = f^".opt" and fb = f^".byte" in
+ let deps = if opt then [fb;fo] else [fb] in
+ copy_bin srcd radix;
+ rule f ~deps:deps ~prod:f (fun _ _ -> ln_s (radix^best_ext) f)
+
+
+
+(** The real game ... *)
let _ = dispatch begin function
| After_rules -> (* Add our rules after the standard ones. *)
+(** The _build/bin directory isn't done by default *)
+
+ if not (Sys.file_exists "_build/bin") then
+ Command.execute ~quiet:true (ln_s "../bin" "_build");
+
(** Camlp4 extensions *)
rule "ml4ml" ~dep:"%.ml4" ~prod:"%.ml"
(fun env _ ->
let ml4 = env "%.ml4" and ml = env "%.ml" in
- Cmd (S[A camlp4o;T(tags_of_pathname ml4 ++ "p4mod");readable_flag;
- T(tags_of_pathname ml4 ++ "p4option");
- Sh camlp4compat; A"-o"; P ml; A"-impl"; P ml4]));
+ Cmd (S[camlp4o;T(tags_of_pathname ml4 ++ "p4mod");readable_flag;
+ T(tags_of_pathname ml4 ++ "p4option"); camlp4compat;
+ A"-o"; P 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"parsing/grammar.cma");
- flag_and_dep ["is_ml4"; "p4mod"; "use_constr"] (P"parsing/q_constr.cmo");
+ flag_and_dep ["is_ml4"; "p4mod"; "use_grammar"] (P grammar);
+ flag_and_dep ["is_ml4"; "p4mod"; "use_constr"] (P qconstr);
(** Special case of toplevel/mltop.ml4:
- mltop.ml 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"] (A flag_dynlink);
+ flag ["is_mltop"; "p4option"] flag_dynlink;
(*TODO: this is rather ugly for a simple file, we should try to
benefit more from predefined rules *)
@@ -121,19 +189,17 @@ let _ = dispatch begin function
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"-rectypes"; A"-I"; A camlp4lib;
- A"-pp";
- Quote (S [A camlp4o; T(tags_of_pathname ml4 ++ "p4mod");
- A"-DByte"; A"-DHasDynLink"; Sh camlp4compat;
+ Cmd (S [!Options.ocamlc; A"-c"; A"-pp";
+ Quote (S [camlp4o; T(tags_of_pathname ml4 ++ "p4mod");
+ A"-DByte"; A"-DHasDynLink"; camlp4compat;
A"-impl"]);
- A"-rectypes"; A"-I"; A camlp4lib;
- Ocaml_utils.ocaml_include_flags ml4;
+ A"-rectypes"; camlp4lib; Ocaml_utils.ocaml_include_flags ml4;
A"-impl"; P ml4]));
-(** All caml files are compiled with -rectypes and +camlp5 *)
+(** All caml files are compiled with -rectypes and +camlp4/5 *)
- flag ["compile"; "ocaml"] (S [A"-rectypes"; A"-I"; A camlp4lib]);
- flag ["link"; "ocaml"] (S [A"-rectypes"; A"-I"; A camlp4lib]);
+ flag ["compile"; "ocaml"] (S [A"-rectypes"; camlp4lib]);
+ flag ["link"; "ocaml"] (S [A"-rectypes"; camlp4lib]);
(** Extra libraries *)
@@ -141,76 +207,85 @@ let _ = dispatch begin function
(** C code for the VM *)
- let headers = List.map (fun s -> "kernel/byterun/"^s)
- ["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";
- "coq_jumptbl.h"]
- in
- dep ["compile"; "c"] headers;
+ dep ["compile"; "c"] c_headers;
flag ["compile"; "c"] (S[A"-ccopt";A"-fno-defer-pop -Wall -Wno-unused"]);
- dep ["link"; "ocaml"; "use_libcoqrun"] ["kernel/byterun/libcoqrun.a"];
-
-(** Generation of coq_jumbtbl.h for the VM *)
+ dep ["link"; "ocaml"; "use_libcoqrun"] [libcoqrun];
- let coqjump = "kernel/byterun/coq_jumptbl.h"
- and coqinstr = "kernel/byterun/coq_instruct.h" in
- let cmd = Printf.sprintf
- "sed -n -e '/^ /s/ \\([A-Z]\\)/ \\&\\&coq_lbl_\\1/gp' -e '/^}/q' %s > %s"
- coqinstr coqjump
- in
- rule "coqjump" ~deps:[coqinstr] ~prod:coqjump
- (fun _ _ -> Cmd (Sh cmd));
+(** VM: Generation of coq_jumbtbl.h and copcodes.ml from coq_instruct.h *)
-(** Generation of opcodes for the VM *)
-
- let copcodes = "kernel/copcodes.ml"
- and coqinstr = "kernel/byterun/coq_instruct.h"
- and script = "kernel/make-opcodes" in
- let cmd = Printf.sprintf
- "sed -n -e '/^enum/p' -e 's/,//g' -e '/^ /p' %s | awk -f %s > %s"
- coqinstr script copcodes
- in
- rule "copcodes" ~deps:[coqinstr;script] ~prod:copcodes
- (fun _ _ -> Cmd (Sh cmd));
+ 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 *)
- let tolink = "scripts/tolink.ml" in
- let core_cma_s = String.concat " " core_cma in
- let core_mllib_s = String.concat " " core_mllib in
- let cmd =
- "(echo \'let copts = \"-cclib -lcoqrun\"\'; "^
- "echo \'let core_libs = \"config/coq_config.cmo "^core_cma_s^"\"\'; "^
- "echo \'let core_objs = \"Coq_config `cat "^core_mllib_s^"`\"\'; "^
- "echo \'let ide = \"`cat ide/ide.mllib`\"\' " ^
- ") > " ^ tolink
- in
- rule "tolink.ml" ~deps:core_mllib ~prod:tolink
- (fun _ _ -> Cmd (Sh cmd));
+ rule "tolink.ml" ~deps:(ide_mllib::core_mllib) ~prod:tolink
+ (fun _ _ ->
+ let cat s = String.concat " " (read_file s) in
+ let core_mods = String.concat " " (List.map 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 = \""^coqconfig^".cmo "^core_cmas^"\"\n";
+ "let core_objs = \"Coq_config "^core_mods^"\"\n";
+ "let ide = \""^ide_mods^"\"\n"],
+ tolink));
(** Coqtop *)
- let coqtopopt = "bin/coqtop.opt"
- and coqtopbyte = "bin/coqtop.byte" in
- let deps = ["scripts/coqmktop.native";"kernel/byterun/libcoqrun.a"] in
- let depsopt = [ "config/coq_config.cmx"] @ deps @ core_cmxa
- and depsbyte = [ "config/coq_config.cmo"] @ deps @ core_cma
- in begin
- rule "coqtop.opt" ~deps:depsopt ~prod:coqtopopt
+ let coqtopo = coqtop^".opt" and coqtopb = coqtop^".byte" in
+ let depso = [coqmktop;libcoqrun;coqconfig^".cmx"] @ core_cmxa
+ and depsb = [coqmktop;libcoqrun;coqconfig^".cmo"] @ core_cma
+ in
+ if opt then rule coqtopo ~prod:coqtopo ~deps:depso
(fun _ _ ->
- Cmd (S [P "scripts/coqmktop.native";A"-boot";A"-opt";
- Ocaml_utils.ocaml_include_flags coqtopopt;
- A"-o";P coqtopopt]));
- rule "coqtop.byte" ~deps:depsbyte ~prod:coqtopbyte
+ Cmd (S [P coqmktop;A"-boot";A"-opt";
+ Ocaml_utils.ocaml_include_flags coqtopo; A"-o";P coqtopo]));
+ rule coqtopb ~prod:coqtopb ~deps:depsb
(fun _ _ ->
- Cmd (S [P "scripts/coqmktop.native";A"-boot";A"-top";
- Ocaml_utils.ocaml_include_flags coqtopbyte;
- A"-o";P coqtopbyte]));
- end;
+ Cmd (S [P coqmktop;A"-boot";A"-top";
+ Ocaml_utils.ocaml_include_flags coqtopb; A"-o";P coqtopb]));
+ rule coqtop ~prod:coqtop ~deps:(coqtopb :: if opt then [coqtopo] else [])
+ (fun _ _ -> ln_s ("coqtop"^best_ext) coqtop);
+
+(** Coqmktop *)
+
+ copy_bin_alias "scripts/" "coqmktop";
+
+(** Coqc *)
+
+ copy_bin_alias "scripts/" "coqc";
+
+(** Coqdep *)
+
+ copy_rule ("tools/coqdep_boot"^best_oext) coqdep_boot;
+ copy_rule ("tools/coqdep"^best_oext) coqdep;
+
+(** Misc binaries *)
-(** bin : directory bin doesn't get made by default ??!! *)
+ copy_rule ("tools/coqdoc/main"^best_oext) coqdoc;
+ copy_rule ("tools/coqwc"^best_oext) coqwc;
+ copy_rule ("tools/coq_makefile"^best_oext) coqmakefile;
+ copy_rule ("tools/coq_tex"^best_oext) coqtex;
+ copy_rule ("tools/gallina"^best_oext) gallina;
- rule "bin dir" ~prod:"bin/.foo" (fun _ _ -> Cmd (Sh "mkdir -p bin && touch bin/.foo"));
+(* TODO: coqide, coqchk *)
| _ -> ()