From c046b33aa98537a157becad80dafd1ebf4e01534 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 8 Dec 2009 15:01:19 +0000 Subject: Fix the build of coq via ocamlbuild - no more plugins/interface - a few missing files in theories.itarget - a few things required Unix now git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12572 85f007b7-540e-0410-9357-904b9bb8a0f7 --- _tags | 6 +++++- myocamlbuild.ml | 12 +++++++----- plugins/_tags | 4 ---- plugins/pluginsbyte.itarget | 2 -- plugins/pluginsopt.itarget | 2 -- plugins/pluginsvo.itarget | 2 -- theories/theories.itarget | 2 ++ 7 files changed, 14 insertions(+), 16 deletions(-) diff --git a/_tags b/_tags index 97957e81ea..6f83b4ef3a 100644 --- a/_tags +++ b/_tags @@ -9,12 +9,16 @@ : use_str : use_str : use_str, use_unix, use_gramlib - : use_nums + : use_nums, use_unix ## tags for ide : thread, ide +## tags for grammar.cm* + + : use_unix + ## tags for camlp4 files <**/*.ml4>: is_ml4 diff --git a/myocamlbuild.ml b/myocamlbuild.ml index 963adcc7c1..f7c014aba3 100644 --- a/myocamlbuild.ml +++ b/myocamlbuild.ml @@ -124,18 +124,18 @@ let theoriesv = let vo = string_list_of_file "theories/theories.itarget" in List.map (fun s -> "theories/"^(Filename.chop_suffix s "o")) vo -let contribv = +let pluginsv = let vo = string_list_of_file "plugins/pluginsvo.itarget" in List.map (fun s -> "plugins/"^(Filename.chop_suffix s "o")) vo -let contribmllib = +let pluginsmllib = let cma = string_list_of_file "plugins/pluginsbyte.itarget" in List.map (fun s -> "plugins/"^(Filename.chop_suffix s ".cma")^".mllib") cma (** for correct execution of coqdep_boot, source files should have been imported in _build (and NMake.v should have been created). *) -let coqdepdeps = theoriesv @ contribv @ contribmllib +let coqdepdeps = theoriesv @ pluginsv @ pluginsmllib let coqtop = "toplevel/coqtop" let coqide = "ide/coqide" @@ -209,9 +209,11 @@ let incl f = Ocaml_utils.ocaml_include_flags f let cmd cl = (fun _ _ -> (Cmd (S cl))) let initial_actions () = begin - make_bin_links all_binaries; - (** We "pre-create" a few subdirs in _build to please coqtop *) + (** We "pre-create" a few subdirs in _build *) Shell.mkdir_p (!_build^"/dev"); + Shell.mkdir_p (!_build^"/bin"); + Shell.mkdir_p (!_build^"/plugins/micromega"); + make_bin_links all_binaries; end let extra_rules () = begin diff --git a/plugins/_tags b/plugins/_tags index 6d28450fd4..f95e0c5b80 100644 --- a/plugins/_tags +++ b/plugins/_tags @@ -3,8 +3,6 @@ "cc/g_congruence.ml4": use_grammar "setoid_ring/newring.ml4": use_grammar "dp/g_dp.ml4": use_grammar -"interface/centaur.ml4": use_grammar -"interface/debug_tac.ml4": use_grammar "quote/g_quote.ml4": use_grammar "subtac/equations.ml4": use_grammar, use_extend "subtac/g_eterm.ml4": use_grammar @@ -23,12 +21,10 @@ "groebner/ideal.ml4": use_refutpat "groebner/groebner.ml4": use_grammar - "cc": include "extraction": include "firstorder": include "funind": include -"interface": include "micromega": include "quote": include "romega": include diff --git a/plugins/pluginsbyte.itarget b/plugins/pluginsbyte.itarget index 7e0a777874..7ca8020dc1 100644 --- a/plugins/pluginsbyte.itarget +++ b/plugins/pluginsbyte.itarget @@ -3,8 +3,6 @@ setoid_ring/newring_plugin.cma extraction/extraction_plugin.cma firstorder/ground_plugin.cma rtauto/rtauto_plugin.cma -interface/coqinterface_plugin.cma -interface/coqparser_plugin.cma fourier/fourier_plugin.cma romega/romega_plugin.cma omega/omega_plugin.cma diff --git a/plugins/pluginsopt.itarget b/plugins/pluginsopt.itarget index e8e7868b76..5206271157 100644 --- a/plugins/pluginsopt.itarget +++ b/plugins/pluginsopt.itarget @@ -3,8 +3,6 @@ setoid_ring/newring_plugin.cmxa extraction/extraction_plugin.cmxa firstorder/ground_plugin.cmxa rtauto/rtauto_plugin.cmxa -interface/coqinterface_plugin.cmxa -interface/coqparser_plugin.cmxa fourier/fourier_plugin.cmxa romega/romega_plugin.cmxa omega/omega_plugin.cmxa diff --git a/plugins/pluginsvo.itarget b/plugins/pluginsvo.itarget index af4d233102..14c2880051 100644 --- a/plugins/pluginsvo.itarget +++ b/plugins/pluginsvo.itarget @@ -8,8 +8,6 @@ fourier/Fourier.vo funind/Recdef.vo groebner/GroebnerR.vo groebner/GroebnerZ.vo -interface/CoqInterface.vo -#interface/CoqParser.vo (should not be compiled) micromega/CheckerMaker.vo micromega/EnvRing.vo micromega/Env.vo diff --git a/theories/theories.itarget b/theories/theories.itarget index 019047ef5f..99b059f510 100644 --- a/theories/theories.itarget +++ b/theories/theories.itarget @@ -42,6 +42,7 @@ Classes/SetoidAxioms.vo Classes/SetoidClass.vo Classes/SetoidDec.vo Classes/SetoidTactics.vo +Classes/RelationPairs.vo FSets/FMapAVL.vo FSets/FMapFacts.vo @@ -89,6 +90,7 @@ Structures/DecidableType2.vo Structures/DecidableType2Ex.vo Structures/DecidableType2Facts.vo Structures/OrderTac.vo +Structures/GenericMinMax.vo Init/Datatypes.vo Init/Logic_Type.vo -- cgit v1.2.3