aboutsummaryrefslogtreecommitdiffhomepage
path: root/scripts/coqmktop.ml
diff options
context:
space:
mode:
Diffstat (limited to 'scripts/coqmktop.ml')
-rw-r--r--scripts/coqmktop.ml59
1 files changed, 12 insertions, 47 deletions
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index c6a442761..239b45fab 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -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 ide = split_list Tolink.ide
-let core_objs =
- libobjs @ lib @ kernel @ library @ pretyping @ interp @ parsing @
- proofs @ tactics
+let core_objs = split_list Tolink.core_objs
+let core_libs = split_list Tolink.core_libs
-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 =
+(* 3. Toplevel objects *)
+let camlp4topobjs =
["camlp4_top.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"; "q_util.cmo"; "q_coqast.cmo" ]
-let topobjs = camlp4objs
+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
@@ -102,7 +79,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 +90,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 +150,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