diff options
| -rw-r--r-- | Makefile.common | 3 | ||||
| -rw-r--r-- | _tags | 7 | ||||
| -rwxr-xr-x | build | 26 | ||||
| -rw-r--r-- | coq.itarget | 16 | ||||
| -rw-r--r-- | kernel/byterun/coq_instruct.h | 4 | ||||
| -rw-r--r-- | myocamlbuild.ml | 281 |
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 @@ -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 @@ -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 *) | _ -> () |