Skip to content
Browse files

A few fixes to the build system (mostly for ocamlbuild)

 * vars.mli was mentionning Term instead of Constr, leading to a dep cycle
 * Having a file named toplevel/toplevel.ml isn't a good idea when we also
   have a toplevel/toplevel.mllib that ought to produce a toplevel.cma.
   We rename toplevel.ml into Coqloop.ml
 * Extra cleanup of toplevel.mllib :
   - Ppextra isn't anywhere around (?!)
   - Ppvernac was mentionned twice, and rather belongs to printing.mllib anyway
   - Vernacexpr is a .mli and shouldn't appear in an .mllib
 * During the link, printing.cma now comes after parsing.cma (Ppvernac uses Egramml)
 * A few extra -threads in ocamlbuild files (btw, it's a bit sad to need -thread
   for coqchk).
  • Loading branch information...
1 parent 9f00530 commit 4759f60b04a278ecd46c8a120340ba55b185c6d1 @letouzey letouzey committed Dec 16, 2013
View
2 Makefile.common
@@ -156,7 +156,7 @@ BYTERUN:=$(addprefix kernel/byterun/, \
CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \
pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \
- printing/printing.cma parsing/parsing.cma tactics/tactics.cma \
+ parsing/parsing.cma printing/printing.cma tactics/tactics.cma \
toplevel/toplevel.cma parsing/highparsing.cma tactics/hightactics.cma
GRAMMARCMA:=tools/compat5.cmo grammar/grammar.cma
View
4 _tags
@@ -9,10 +9,10 @@
<tools/coq_makefile.{native,byte}> : use_str, use_unix
<tools/coqdoc/main.{native,byte}> : use_str
<ide/coqide_main.{native,byte}> : use_str, use_unix, ide
-<checker/main.{native,byte}> : use_str, use_unix
+<checker/main.{native,byte}> : use_str, use_unix, thread
<plugins/micromega/csdpcert.{native,byte}> : use_nums, use_unix
<tools/mkwinapp.{native,byte}> : use_unix
-<tools/fake_ide.{native,byte}> : use_unix
+<tools/fake_ide.{native,byte}> : use_unix, use_str
## tags for ide
View
2 kernel/vars.mli
@@ -7,7 +7,7 @@
(************************************************************************)
open Names
-open Term
+open Constr
open Context
(** {6 Occur checks } *)
View
8 myocamlbuild.ml
@@ -105,7 +105,7 @@ let _build = Options.build_dir
let core_libs =
["lib/clib"; "lib/lib"; "kernel/kernel"; "library/library";
"pretyping/pretyping"; "interp/interp"; "proofs/proofs";
- "printing/printing"; "parsing/parsing"; "tactics/tactics";
+ "parsing/parsing"; "printing/printing"; "tactics/tactics";
"toplevel/toplevel"; "parsing/highparsing"; "tactics/hightactics"]
let core_cma = List.map (fun s -> s^".cma") core_libs
let core_cmxa = List.map (fun s -> s^".cmxa") core_libs
@@ -301,7 +301,7 @@ let extra_rules () = begin
(** All caml files are compiled with +camlp4/5
and ide files need +lablgtk2 *)
- flag ["compile"; "ocaml"] (S [A"-rectypes"; camlp4incl]);
+ flag ["compile"; "ocaml"] (S [A"-thread";A"-rectypes"; camlp4incl]);
flag ["link"; "ocaml"] (S [A"-rectypes"; camlp4incl]);
flag ["ocaml"; "ide"; "compile"] lablgtkincl;
flag ["ocaml"; "ide"; "link"] lablgtkincl;
@@ -389,9 +389,9 @@ let extra_rules () = begin
if not w32 then N else S ([A"-camlbin";A w32bin;A "-ccopt";P w32ico])
in
if opt then rule fo ~prod:fo ~deps:(depsall@depso) ~insert:`top
- (cmd [P coqmktop_boot;w32flag;A"-boot";A"-opt";incl fo;camlp4incl;A"-o";Px fo]);
+ (cmd [P coqmktop_boot;w32flag;A"-boot";A"-opt";incl fo;A"-thread";camlp4incl;A"-o";Px fo]);
rule fb ~prod:fb ~deps:(depsall@depsb) ~insert:`top
- (cmd [P coqmktop_boot;w32flag;A"-boot";A"-top";incl fb;camlp4incl;A"-o";Px fb]);
+ (cmd [P coqmktop_boot;w32flag;A"-boot";A"-top";incl fb;A"-thread";camlp4incl;A"-o";Px fb]);
in
(** Coq files dependencies *)
View
1 printing/ppvernac.ml
@@ -9,7 +9,6 @@
open Pp
open Names
-(* open Compat *)
open Errors
open Util
open Extend
View
18 printing/ppvernac.mli
@@ -6,22 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Pp
-open Genarg
-open Vernacexpr
-open Names
-open Nameops
-open Nametab
-open Ppconstr
-open Pptactic
-open Glob_term
-open Pcoq
-open Libnames
-open Ppextend
-open Topconstr
-
(** Prints a vernac expression *)
-val pr_vernac_body : vernac_expr -> std_ppcmds
+val pr_vernac_body : Vernacexpr.vernac_expr -> Pp.std_ppcmds
(** Prints a vernac expression and closes it with a dot. *)
-val pr_vernac : vernac_expr -> std_ppcmds
+val pr_vernac : Vernacexpr.vernac_expr -> Pp.std_ppcmds
View
1 printing/printing.mllib
@@ -5,3 +5,4 @@ Printer
Pptactic
Printmod
Prettyp
+Ppvernac
View
0 toplevel/toplevel.ml → toplevel/coqloop.ml
File renamed without changes.
View
0 toplevel/toplevel.mli → toplevel/coqloop.mli
File renamed without changes.
View
4 toplevel/coqtop.ml
@@ -401,7 +401,7 @@ let init arglist =
if !batch_mode then mt ()
else str "Error during initialization:" ++ fnl ()
in
- fatal_error (msg ++ Toplevel.print_toplevel_error any)
+ fatal_error (msg ++ Coqloop.print_toplevel_error any)
end;
if !batch_mode then begin
flush_all();
@@ -425,7 +425,7 @@ let start () =
else if !Flags.coq_slave_mode > 0 then
Stm.slave_main_loop ()
else
- Toplevel.loop();
+ Coqloop.loop();
(* Initialise and launch the Ocaml toplevel *)
Coqinit.init_ocaml_path();
Mltop.ocaml_toploop();
View
2 toplevel/coqtop.mli
@@ -9,7 +9,7 @@
(** The Coq main module. The following function [start] will parse the
command line, print the banner, initialize the load path, load the input
state, load the files given on the command line, load the ressource file,
- produce the output state if any, and finally will launch [Toplevel.loop]. *)
+ produce the output state if any, and finally will launch [Coqloop.loop]. *)
val init_toplevel : string list -> unit
View
6 toplevel/toplevel.mllib
@@ -2,9 +2,6 @@ Himsg
Cerrors
Class
Locality
-Vernacexpr
-Ppextra
-Ppvernac
Metasyntax
Auto_ind_decl
Search
@@ -15,7 +12,6 @@ Obligations
Command
Classes
Record
-Ppvernac
Vernacinterp
Mltop
Vernacentries
@@ -24,7 +20,7 @@ Stm
Whelp
Vernac
Ide_slave
-Toplevel
Usage
+Coqloop
Coqinit
Coqtop

0 comments on commit 4759f60

Please sign in to comment.
Something went wrong with that request. Please try again.