From 26ad56149f93939b122e94bf54a5f0b4f3ec9f98 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 17 Oct 2018 15:40:59 +0200 Subject: [doc] [build] Remove ocamlbuild leftovers. We had a brief leftovers of the ocamlbuild experiment that are not relevant anymore as it was removed from the tree a few years ago. p.s: The amount of cruft we have in the `dev/build/windows` folder is staggering, see for example what `git grep ocamlbuild` returns. --- .gitignore | 1 - Makefile | 2 +- dev/doc/build-system.txt | 8 +++----- dev/doc/ocamlbuild.txt | 30 ------------------------------ tools/coq_makefile.ml | 2 +- 5 files changed, 5 insertions(+), 38 deletions(-) delete mode 100644 dev/doc/ocamlbuild.txt diff --git a/.gitignore b/.gitignore index 05869e2a0c..63da6b4d0e 100644 --- a/.gitignore +++ b/.gitignore @@ -50,7 +50,6 @@ TAGS bin/ _build_ci _build -myocamlbuild_config.ml config/Makefile config/coq_config.ml config/coq_config.py diff --git a/Makefile b/Makefile index a15870faca..b74e4e5d4f 100644 --- a/Makefile +++ b/Makefile @@ -261,7 +261,7 @@ cacheclean: find theories plugins test-suite -name '.*.aux' -exec rm -f {} + cleanconfig: - rm -f config/Makefile config/coq_config.ml myocamlbuild_config.ml dev/ocamldebug-coq dev/camlp5.dbg config/Info-*.plist + rm -f config/Makefile config/coq_config.ml dev/ocamldebug-coq dev/camlp5.dbg config/Info-*.plist distclean: clean cleanconfig cacheclean timingclean diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt index fd3101613a..8cefe699cc 100644 --- a/dev/doc/build-system.txt +++ b/dev/doc/build-system.txt @@ -140,11 +140,9 @@ New files For a new file, in most cases, you just have to add it to the proper file list(s): - For .ml, in the corresponding .mllib (e.g. kernel/kernel.mllib) - These files are also used by the experimental ocamlbuild plugin, - which is quite touchy about them : be careful with order, - duplicated entries, whitespace errors, and do not mention .mli there. - If module B depends on module A, then B should be after A in the .mllib - file. + Be careful with order, duplicated entries, whitespace errors, and + do not mention .mli there. If module B depends on module A, then B + should be after A in the .mllib file. - For .v, in the corresponding vo.itarget (e.g theories/Init/vo.itarget) - The definitions in Makefile.common might have to be adapted too. - If your file needs a specific rule, add it to Makefile.build diff --git a/dev/doc/ocamlbuild.txt b/dev/doc/ocamlbuild.txt deleted file mode 100644 index efedbc506e..0000000000 --- a/dev/doc/ocamlbuild.txt +++ /dev/null @@ -1,30 +0,0 @@ -Ocamlbuild & Coq ----------------- - -A quick note in case someone else gets interested someday in compiling -Coq via ocamlbuild : such an experimental build system has existed -in the past (more or less maintained from 2009 to 2013), in addition -to the official build system via gnu make. But this build via -ocamlbuild has been severly broken since early 2014 (and don't work -in 8.5, for instance). This experiment has attracted very limited -interest from other developers over the years, and has been quite -cumbersome to maintain, so it is now officially discontinued. -If you want to have a look at the files of this build system -(especially myocamlbuild.ml), you can fetch : - - my last effort at repairing this build system (up to coqtop.native) : - https://github.com/letouzey/coq-wip/tree/ocamlbuild-partial-repair - - coq official v8.5 branch (recent but broken) - - coq v8.4 branch(less up-to-date, but works). - -For the record, the three main drawbacks of this experiments were: - - recurrent issues with circularities reported by ocamlbuild - (even though make was happy) during the evolution of Coq sources - - no proper support of parallel build - - quite slow re-traversal of already built things -See the two corresponding bug reports on Mantis, or -https://github.com/ocaml/ocamlbuild/issues/52 - -As an interesting feature, I successfully used this to cross-compile -Coq 8.4 from linux to win32 via mingw. - -Pierre Letouzey, june 2016 diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index d91c4f0b34..7bb1390cad 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -46,7 +46,7 @@ let usage_coq_makefile () = \n\ \n[file.v]: Coq file to be compiled\ \n[file.ml[i4]?]: Objective Caml file to be compiled\ -\n[file.ml{lib,pack}]: ocamlbuild file that describes a Objective Caml\ +\n[file.ml{lib,pack}]: ocamlbuild-style file that describes a Objective Caml\ \n library/module\ \n[any] : subdirectory that should be \"made\" and has a Makefile itself\ \n to do so. Very fragile and discouraged.\ -- cgit v1.2.3