summaryrefslogtreecommitdiff
path: root/scripts
diff options
context:
space:
mode:
Diffstat (limited to 'scripts')
-rw-r--r--scripts/coqc.ml13
-rw-r--r--scripts/coqmktop.ml82
2 files changed, 34 insertions, 61 deletions
diff --git a/scripts/coqc.ml b/scripts/coqc.ml
index 34025ec9..676e9e51 100644
--- a/scripts/coqc.ml
+++ b/scripts/coqc.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqc.ml,v 1.25.2.3 2004/09/04 10:34:56 herbelin Exp $ *)
+(* $Id: coqc.ml 7747 2005-12-28 10:28:41Z herbelin $ *)
(* Afin de rendre Coq plus portable, ce programme Caml remplace le script
coqc.
@@ -148,10 +148,15 @@ let parse_args () =
| [] -> usage ()
end
| "-R" as o :: s :: t :: rem -> parse (cfiles,t::s::o::args) rem
- | ("-notactics"|"-debug"|"-nolib"|"-batch"|"-nois"
+
+ | ("-notactics"|"-debug"|"-nolib"
+ | "-debugVM"|"-alltransp"|"-VMno"
+ |"-batch"|"-nois"
|"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet"
- |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-translate"|"-strict-implicit"
- |"-dont-load-proofs"|"-impredicative-set" as o) :: rem ->
+ |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-translate" |"-strict-implicit"
+ |"-dont-load-proofs"|"-impredicative-set"|"-vm"
+ | "-unboxed-values" | "-unboxed-definitions" | "-draw-vm-instr"
+ as o) :: rem ->
parse (cfiles,o::args) rem
| ("-v"|"--version") :: _ ->
Usage.version ()
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index ccb06769..dec302e7 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqmktop.ml,v 1.28.2.2 2005/11/04 08:20:57 herbelin Exp $ *)
+(* $Id: coqmktop.ml 7538 2005-11-08 17:14:52Z herbelin $ *)
(* coqmktop is a script to link Coq, analogous to ocamlmktop.
The command line contains options specific to coqmktop, options for the
@@ -19,49 +19,26 @@ open Unix
(* 1. Core objects *)
let ocamlobjs = ["unix.cma"]
let dynobjs = ["dynlink.cma"]
-let camlp4objs = [(*"odyl.cma"; "camlp4.cma";*) "gramlib.cma"]
-let configobjs = ["coq_config.cmo"]
-let libobjs = ocamlobjs @ camlp4objs @ configobjs
+let camlp4objs = ["gramlib.cma"]
+let libobjs = ocamlobjs @ camlp4objs
let spaces = Str.regexp "[ \t\n]+"
-let split_cmo l = Str.split spaces l
+let split_list l = Str.split spaces l
-let lib = split_cmo Tolink.lib
-let kernel = split_cmo Tolink.kernel
-let library = split_cmo Tolink.library
-let pretyping = split_cmo Tolink.pretyping
-let interp = split_cmo Tolink.interp
-let parsing = split_cmo Tolink.parsing
-let proofs = split_cmo Tolink.proofs
-let tactics = split_cmo Tolink.tactics
-let toplevel = split_cmo Tolink.toplevel
-let highparsing = split_cmo Tolink.highparsing
-let highparsingnew = split_cmo Tolink.highparsingnew
-let ide = split_cmo Tolink.ide
+let copts = split_list Tolink.copts
+let core_objs = split_list Tolink.core_objs
+let core_libs = split_list Tolink.core_libs
+let ide = split_list Tolink.ide
-let core_objs =
- libobjs @ lib @ kernel @ library @ pretyping @ interp @ parsing @
- proofs @ tactics
-
-let core_libs =
- libobjs @ [ "lib/lib.cma" ; "kernel/kernel.cma" ; "library/library.cma" ;
- "pretyping/pretyping.cma" ; "interp/interp.cma" ; "parsing/parsing.cma" ;
- "proofs/proofs.cma" ; "tactics/tactics.cma" ]
-
-(* 3. Files only in coqsearchisos (if option -searchisos is used) *)
-let coqsearch = ["version_searchisos.cmo"; "cmd_searchisos_line.cmo"]
-
-(* 4. Toplevel objects *)
-let camlp4objs =
- ["camlp4_top.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"; "q_util.cmo"; "q_coqast.cmo" ]
-let topobjs = camlp4objs
+(* 3. Toplevel objects *)
+let camlp4topobjs =
+ ["camlp4_top.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"]
+let topobjs = camlp4topobjs
let gramobjs = []
let notopobjs = gramobjs
-(* 5. High-level tactics objects *)
-let hightactics =
- (split_cmo Tolink.hightactics) @ (split_cmo Tolink.contrib)
+(* 4. High-level tactics objects *)
(* environment *)
let src_coqtop = ref Coq_config.coqtop
@@ -73,7 +50,7 @@ let coqide = ref false
let echo = ref false
let src_dirs () =
- [ []; [ "config" ]; [ "toplevel" ] ] @
+ [ []; ["kernel";"byterun"]; [ "config" ]; [ "toplevel" ] ] @
if !coqide then [[ "ide" ]] else []
let includes () =
@@ -89,8 +66,10 @@ let native_suffix f =
(Filename.chop_suffix f ".cmo") ^ ".cmx"
else if Filename.check_suffix f ".cma" then
(Filename.chop_suffix f ".cma") ^ ".cmxa"
- else
- failwith ("File "^f^" has not extension .cmo or .cma")
+ else
+ if Filename.check_suffix f ".a" then f
+ else
+ failwith ("File "^f^" has not extension .cmo, .cma or .a")
(* Transforms a file name in the corresponding Caml module name. *)
let rem_ext_regexpr = Str.regexp "\\(.*\\)\\.\\(cm..?\\|ml\\)"
@@ -102,7 +81,6 @@ let module_of_file name =
(* Build the list of files to link and the list of modules names *)
let files_to_link userfiles =
let dyn_objs = if not !opt then dynobjs else [] in
- let command_objs = if !searchisos then coqsearch else [] in
let toplevel_objs =
if !top then topobjs else if !opt then notopobjs else [] in
let ide_objs = if !coqide then
@@ -114,17 +92,8 @@ let files_to_link userfiles =
"ide/ide.cma" ]
else []
in
- let objs =
- core_objs @ dyn_objs @ toplevel @ highparsing @ highparsingnew @
- command_objs @ hightactics @ toplevel_objs @ ide_objs
- and libs =
- core_libs @ dyn_objs @
- [ "toplevel/toplevel.cma" ; "parsing/highparsing.cma" ;
- "parsing/highparsingnew.cma" ] @
- command_objs @ [ "tactics/hightactics.cma" ; "contrib/contrib.cma" ] @
- toplevel_objs @
- ide_libs
- in
+ let objs = dyn_objs @ libobjs @ core_objs @ toplevel_objs @ ide_objs
+ and libs = dyn_objs @ libobjs @ core_libs @ toplevel_objs @ ide_libs in
let objstolink,libstolink =
if !opt then
((List.map native_suffix objs) @ userfiles,
@@ -183,8 +152,6 @@ let parse_args () =
| "-opt" :: rem -> opt := true ; parse (op,fl) rem
| "-full" :: rem -> full := true ; parse (op,fl) rem
| "-top" :: rem -> top := true ; parse (op,fl) rem
- | "-searchisos" :: rem ->
- searchisos := true; parse (op,fl) rem
| "-ide" :: rem ->
coqide := true; parse (op,fl) rem
| "-v8" :: rem -> parse (op,fl) rem
@@ -199,7 +166,8 @@ let parse_args () =
parse ((List.rev(List.flatten (List.map (fun d -> ["-I";d])
(all_subdirs a))))@op,fl) rem
| "-R" :: [] -> usage ()
- | ("-compact"|"-g"|"-p"|"-thread" as o) :: rem -> parse (o::op,fl) rem
+ | ("-noassert"|"-compact"|"-g"|"-p"|"-thread" as o) :: rem ->
+ parse (o::op,fl) rem
| ("-h"|"--help") :: _ -> usage ()
| f :: rem ->
if Filename.check_suffix f ".ml"
@@ -230,7 +198,6 @@ let clean file =
let all_modules_in_dir dir =
try
let lst = ref []
- and stg = ref ""
and dh = Unix.opendir dir in
try
while true do
@@ -331,11 +298,12 @@ let main () =
(* the list of the loaded modules *)
let main_file = create_tmp_main_file modules in
try
- let args = options @ (includes ()) @ tolink @ dynlink @ [ main_file ] in
+ let args =
+ options @ (includes ()) @ copts @ tolink @ dynlink @ [ main_file ] in
(* add topstart.cmo explicitly because we shunted ocamlmktop wrapper *)
let args = if !top then args @ [ "topstart.cmo" ] else args in
(* Now, with the .cma, we MUST use the -linkall option *)
- let command = String.concat " " ((prog^" -linkall")::args) in
+ let command = String.concat " " (prog::args) in
if !echo then
begin
print_endline command;