From 251b34ac94d8797637b3ca5acce5db593950d0c5 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sun, 18 Sep 2011 21:51:16 +0000
Subject: avoid dependency nightmare by creating coqdep_{lexer,common}.mli

 Sequel to commit 14476 : in fact, even with "tools" in .PHONY,
 we still may have coqdep stuff being recompiled in a "make"
 that follows a successful "make". This seems to related to
 the hacks I've introduced to prevent ocamlopt from erasing
 and recreating .cmi when there's no .mli around
 (cf. comment around line 823 in Makefile.build).

 Scenario:
  - First we build coqdep_boot directly out of coqdep_lexer.ml and co.
    When ocamlopt is around, this creates some .cmx and .cmi,
    but no .cmo.
  - Later we build coqdep, which need coqdep_lexer.cmx and co.
    Now "make" checks whether these .cmx are up-to-date.
    But our hacks made these .cmx depend on the corresponding .cmi.
    Then "make" checks whether these .cmi are up-to-date.
    But our hacks made these .cmi depend on the corresponding .cmo.
    These .cmo doesn't exist yet, we run ocamlc, which recreates
    the .cmi with same content but a different timestamp.
    For some strange reason, even with refreshed .cmi, the .cmx
    are not remade by this run, but will be on the next run.

 Conclusion: what a mess. Implicit rules about .cmx / .cmo / .cmi
 should be improved, but I see currently no simple solution.

 In the meantime, an simple ad-hoc fix is to create these two .mli ...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14479 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tools/coqdep_lexer.mli | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)
 create mode 100644 tools/coqdep_lexer.mli

(limited to 'tools/coqdep_lexer.mli')

diff --git a/tools/coqdep_lexer.mli b/tools/coqdep_lexer.mli
new file mode 100644
index 000000000..260586270
--- /dev/null
+++ b/tools/coqdep_lexer.mli
@@ -0,0 +1,23 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+type mL_token = Use_module of string
+
+type coq_token =
+    Require of string list list
+  | RequireString of string
+  | Declare of string list
+  | Load of string
+
+exception Fin_fichier
+exception Syntax_error of int * int
+
+val coq_action : Lexing.lexbuf -> coq_token
+val caml_action : Lexing.lexbuf -> mL_token
+val mllib_list : Lexing.lexbuf -> string list
+val ocamldep_parse : Lexing.lexbuf -> string list
-- 
cgit v1.2.3