From 1419bb9ddd1299673707404f1f35b4904648760b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 12 Jul 2018 18:48:28 +0200 Subject: [dev] Autogenerate OCaml dev files. For now we only copy the templates, but we could do more fancy stuff. This helps to be compatible with build systems that take care of these files automatically, see: https://github.com/coq/coq/pull/6857#discussion_r202096579 --- .github/CODEOWNERS | 2 +- .gitignore | 4 + .merlin | 54 ---- .merlin.in | 54 ++++ META.coq | 555 --------------------------------------- META.coq.in | 555 +++++++++++++++++++++++++++++++++++++++ Makefile | 9 +- Makefile.build | 2 +- Makefile.dev | 18 +- dev/tools/coqdev.el | 2 +- ide/.merlin | 6 - ide/.merlin.in | 6 + plugins/.merlin | 1 - plugins/.merlin.in | 1 + test-suite/unit-tests/.merlin | 6 - test-suite/unit-tests/.merlin.in | 6 + 16 files changed, 652 insertions(+), 629 deletions(-) delete mode 100644 .merlin create mode 100644 .merlin.in delete mode 100644 META.coq create mode 100644 META.coq.in delete mode 100644 ide/.merlin create mode 100644 ide/.merlin.in delete mode 100644 plugins/.merlin create mode 100644 plugins/.merlin.in delete mode 100644 test-suite/unit-tests/.merlin create mode 100644 test-suite/unit-tests/.merlin.in diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 192a2b181..042e18bd0 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -313,7 +313,7 @@ /configure* @ejgallego -/META.coq @ejgallego +/META.coq.in @ejgallego /dev/build/windows @MSoegtropIMC # Secondary maintainer @maximedenes diff --git a/.gitignore b/.gitignore index 14ec71b93..0e41d6a77 100644 --- a/.gitignore +++ b/.gitignore @@ -179,3 +179,7 @@ test-suite/.nra.cache plugins/ssr/ssrparser.ml plugins/ssr/ssrvernac.ml + +# ocaml dev files +.merlin +META.coq diff --git a/.merlin b/.merlin deleted file mode 100644 index 404a7e793..000000000 --- a/.merlin +++ /dev/null @@ -1,54 +0,0 @@ -FLG -rectypes -thread -safe-string -w +a-4-9-27-41-42-44-45-48-50 - -S clib -B clib -S config -B config -S lib -B lib -S kernel -B kernel -S kernel/byterun -B kernel/byterun -S library -B library -S engine -B engine -S pretyping -B pretyping -S interp -B interp -S proofs -B proofs -S tactics -B tactics -S printing -B printing -S parsing -B parsing -S stm -B stm -S vernac -B vernac -S toplevel -B toplevel -S topbin -B topbin -S plugins/ltac -B plugins/ltac -S API -B API -S ide -B ide - -S tools -B tools -S tools/coqdoc -B tools/coqdoc -S dev -B dev - -S plugins/** -B plugins/** - -PKG threads.posix camlp5 diff --git a/.merlin.in b/.merlin.in new file mode 100644 index 000000000..404a7e793 --- /dev/null +++ b/.merlin.in @@ -0,0 +1,54 @@ +FLG -rectypes -thread -safe-string -w +a-4-9-27-41-42-44-45-48-50 + +S clib +B clib +S config +B config +S lib +B lib +S kernel +B kernel +S kernel/byterun +B kernel/byterun +S library +B library +S engine +B engine +S pretyping +B pretyping +S interp +B interp +S proofs +B proofs +S tactics +B tactics +S printing +B printing +S parsing +B parsing +S stm +B stm +S vernac +B vernac +S toplevel +B toplevel +S topbin +B topbin +S plugins/ltac +B plugins/ltac +S API +B API +S ide +B ide + +S tools +B tools +S tools/coqdoc +B tools/coqdoc +S dev +B dev + +S plugins/** +B plugins/** + +PKG threads.posix camlp5 diff --git a/META.coq b/META.coq deleted file mode 100644 index a7c8da163..000000000 --- a/META.coq +++ /dev/null @@ -1,555 +0,0 @@ -# TODO: Generate automatically with Dune - -description = "The Coq Proof Assistant Plugin API" -version = "8.9" - -directory = "" -requires = "camlp5" - -package "grammar" ( - - description = "Coq Camlp5 Grammar Extensions for Plugins" - version = "8.9" - - requires = "camlp5.gramlib" - directory = "grammar" - - archive(byte) = "grammar.cma" - archive(native) = "grammar.cmxa" -) - -package "config" ( - - description = "Coq Configuration Variables" - version = "8.9" - - directory = "config" - -) - -package "clib" ( - description = "Base General Coq Library" - version = "8.9" - - directory = "clib" - requires = "num, str, unix, threads" - - archive(byte) = "clib.cma" - archive(native) = "clib.cmxa" -) - -package "lib" ( - - description = "Base Coq-Specific Library" - version = "8.9" - - directory = "lib" - - requires = "coq.clib, coq.config" - - archive(byte) = "lib.cma" - archive(native) = "lib.cmxa" - -) - -package "vm" ( - - description = "Coq VM" - version = "8.9" - - directory = "kernel/byterun" - -# We could generate this file at configure time for the share byte -# build path to work properly. -# -# Enable this setting for local byte builds if you want dynamic linking: -# -# linkopts(byte) = "-dllpath path_to_coq/kernel/byterun/ -dllib -lcoqrun" - -# We currently prefer static linking of the VM. - archive(byte) = "libcoqrun.a" - linkopts(byte) = "-custom" -) - -package "kernel" ( - - description = "Coq's Kernel" - version = "8.9" - - directory = "kernel" - - requires = "dynlink, coq.lib, coq.vm" - - archive(byte) = "kernel.cma" - archive(native) = "kernel.cmxa" - -) - -package "library" ( - - description = "Coq Libraries (vo) support" - version = "8.9" - - requires = "coq.kernel" - - directory = "library" - - archive(byte) = "library.cma" - archive(native) = "library.cmxa" - -) - -package "engine" ( - - description = "Coq Tactic Engine" - version = "8.9" - - requires = "coq.library" - directory = "engine" - - archive(byte) = "engine.cma" - archive(native) = "engine.cmxa" - -) - -package "pretyping" ( - - description = "Coq Pretyper" - version = "8.9" - - requires = "coq.engine" - directory = "pretyping" - - archive(byte) = "pretyping.cma" - archive(native) = "pretyping.cmxa" - -) - -package "interp" ( - - description = "Coq Term Interpretation" - version = "8.9" - - requires = "coq.pretyping" - directory = "interp" - - archive(byte) = "interp.cma" - archive(native) = "interp.cmxa" - -) - -package "proofs" ( - - description = "Coq Proof Engine" - version = "8.9" - - requires = "coq.interp" - directory = "proofs" - - archive(byte) = "proofs.cma" - archive(native) = "proofs.cmxa" - -) - -package "parsing" ( - - description = "Coq Parsing Engine" - version = "8.9" - - requires = "camlp5.gramlib, coq.proofs" - directory = "parsing" - - archive(byte) = "parsing.cma" - archive(native) = "parsing.cmxa" - -) - -package "printing" ( - - description = "Coq Printing Engine" - version = "8.9" - - requires = "coq.parsing" - directory = "printing" - - archive(byte) = "printing.cma" - archive(native) = "printing.cmxa" - -) - -package "tactics" ( - - description = "Coq Basic Tactics" - version = "8.9" - - requires = "coq.printing" - directory = "tactics" - - archive(byte) = "tactics.cma" - archive(native) = "tactics.cmxa" - -) - -package "vernac" ( - - description = "Coq Vernacular Interpreter" - version = "8.9" - - requires = "coq.tactics" - directory = "vernac" - - archive(byte) = "vernac.cma" - archive(native) = "vernac.cmxa" - -) - -package "stm" ( - - description = "Coq State Transactional Machine" - version = "8.9" - - requires = "coq.vernac" - directory = "stm" - - archive(byte) = "stm.cma" - archive(native) = "stm.cmxa" - -) - -package "toplevel" ( - - description = "Coq Toplevel" - version = "8.9" - - requires = "coq.stm" - directory = "toplevel" - - archive(byte) = "toplevel.cma" - archive(native) = "toplevel.cmxa" - -) - -package "idetop" ( - - description = "Coq IDE Libraries" - version = "8.9" - - requires = "coq.toplevel" - directory = "ide" - - archive(byte) = "coqidetop.cma" - archive(native) = "coqidetop.cmxa" - -) - -# XXX Depends on way less than toplevel -package "ide" ( - - description = "Coq IDE Libraries" - version = "8.9" - -# XXX Add GTK - requires = "coq.toplevel" - directory = "ide" - - archive(byte) = "ide.cma" - archive(native) = "ide.cmxa" - -) - -package "plugins" ( - - description = "Coq built-in plugins" - version = "8.9" - - directory = "plugins" - - package "ltac" ( - - description = "Coq LTAC Plugin" - version = "8.9" - - requires = "coq.stm" - directory = "ltac" - - archive(byte) = "ltac_plugin.cmo" - archive(native) = "ltac_plugin.cmx" - - ) - - package "tauto" ( - - description = "Coq tauto plugin" - version = "8.9" - - requires = "coq.plugins.ltac" - directory = "ltac" - - archive(byte) = "tauto_plugin.cmo" - archive(native) = "tauto_plugin.cmx" - ) - - package "omega" ( - - description = "Coq omega plugin" - version = "8.9" - - requires = "coq.plugins.ltac" - directory = "omega" - - archive(byte) = "omega_plugin.cmo" - archive(native) = "omega_plugin.cmx" - ) - - package "romega" ( - - description = "Coq romega plugin" - version = "8.9" - - requires = "coq.plugins.omega" - directory = "romega" - - archive(byte) = "romega_plugin.cmo" - archive(native) = "romega_plugin.cmx" - ) - - package "micromega" ( - - description = "Coq micromega plugin" - version = "8.9" - - requires = "num,coq.plugins.ltac" - directory = "micromega" - - archive(byte) = "micromega_plugin.cmo" - archive(native) = "micromega_plugin.cmx" - ) - - package "quote" ( - - description = "Coq quote plugin" - version = "8.9" - - requires = "coq.plugins.ltac" - directory = "quote" - - archive(byte) = "quote_plugin.cmo" - archive(native) = "quote_plugin.cmx" - ) - - package "newring" ( - - description = "Coq newring plugin" - version = "8.9" - - requires = "coq.plugins.quote" - directory = "setoid_ring" - - archive(byte) = "newring_plugin.cmo" - archive(native) = "newring_plugin.cmx" - ) - - package "fourier" ( - - description = "Coq fourier plugin" - version = "8.9" - - requires = "coq.plugins.ltac" - directory = "fourier" - - archive(byte) = "fourier_plugin.cmo" - archive(native) = "fourier_plugin.cmx" - ) - - package "extraction" ( - - description = "Coq extraction plugin" - version = "8.9" - - requires = "coq.plugins.ltac" - directory = "extraction" - - archive(byte) = "extraction_plugin.cmo" - archive(native) = "extraction_plugin.cmx" - ) - - package "cc" ( - - description = "Coq cc plugin" - version = "8.9" - - requires = "coq.plugins.ltac" - directory = "cc" - - archive(byte) = "cc_plugin.cmo" - archive(native) = "cc_plugin.cmx" - ) - - package "ground" ( - - description = "Coq ground plugin" - version = "8.9" - - requires = "coq.plugins.ltac" - directory = "firstorder" - - archive(byte) = "ground_plugin.cmo" - archive(native) = "ground_plugin.cmx" - ) - - package "rtauto" ( - - description = "Coq rtauto plugin" - version = "8.9" - - requires = "coq.plugins.ltac" - directory = "rtauto" - - archive(byte) = "rtauto_plugin.cmo" - archive(native) = "rtauto_plugin.cmx" - ) - - package "btauto" ( - - description = "Coq btauto plugin" - version = "8.9" - - requires = "coq.plugins.ltac" - directory = "btauto" - - archive(byte) = "btauto_plugin.cmo" - archive(native) = "btauto_plugin.cmx" - ) - - package "recdef" ( - - description = "Coq recdef plugin" - version = "8.9" - - requires = "coq.plugins.extraction" - directory = "funind" - - archive(byte) = "recdef_plugin.cmo" - archive(native) = "recdef_plugin.cmx" - ) - - package "nsatz" ( - - description = "Coq nsatz plugin" - version = "8.9" - - requires = "num,coq.plugins.ltac" - directory = "nsatz" - - archive(byte) = "nsatz_plugin.cmo" - archive(native) = "nsatz_plugin.cmx" - ) - - package "natsyntax" ( - - description = "Coq natsyntax plugin" - version = "8.9" - - requires = "" - directory = "syntax" - - archive(byte) = "nat_syntax_plugin.cmo" - archive(native) = "nat_syntax_plugin.cmx" - ) - - package "zsyntax" ( - - description = "Coq zsyntax plugin" - version = "8.9" - - requires = "" - directory = "syntax" - - archive(byte) = "z_syntax_plugin.cmo" - archive(native) = "z_syntax_plugin.cmx" - ) - - package "rsyntax" ( - - description = "Coq rsyntax plugin" - version = "8.9" - - requires = "" - directory = "syntax" - - archive(byte) = "r_syntax_plugin.cmo" - archive(native) = "r_syntax_plugin.cmx" - ) - - package "int31syntax" ( - - description = "Coq int31syntax plugin" - version = "8.9" - - requires = "" - directory = "syntax" - - archive(byte) = "int31_syntax_plugin.cmo" - archive(native) = "int31_syntax_plugin.cmx" - ) - - package "asciisyntax" ( - - description = "Coq asciisyntax plugin" - version = "8.9" - - requires = "" - directory = "syntax" - - archive(byte) = "ascii_syntax_plugin.cmo" - archive(native) = "ascii_syntax_plugin.cmx" - ) - - package "stringsyntax" ( - - description = "Coq stringsyntax plugin" - version = "8.9" - - requires = "coq.plugins.asciisyntax" - directory = "syntax" - - archive(byte) = "string_syntax_plugin.cmo" - archive(native) = "string_syntax_plugin.cmx" - ) - - package "derive" ( - - description = "Coq derive plugin" - version = "8.9" - - requires = "" - directory = "derive" - - archive(byte) = "derive_plugin.cmo" - archive(native) = "derive_plugin.cmx" - ) - - package "ssrmatching" ( - - description = "Coq ssrmatching plugin" - version = "8.9" - - requires = "coq.plugins.ltac" - directory = "ssrmatching" - - archive(byte) = "ssrmatching_plugin.cmo" - archive(native) = "ssrmatching_plugin.cmx" - ) - - package "ssreflect" ( - - description = "Coq ssreflect plugin" - version = "8.9" - - requires = "coq.plugins.ssrmatching" - directory = "ssr" - - archive(byte) = "ssreflect_plugin.cmo" - archive(native) = "ssreflect_plugin.cmx" - ) -) diff --git a/META.coq.in b/META.coq.in new file mode 100644 index 000000000..a7c8da163 --- /dev/null +++ b/META.coq.in @@ -0,0 +1,555 @@ +# TODO: Generate automatically with Dune + +description = "The Coq Proof Assistant Plugin API" +version = "8.9" + +directory = "" +requires = "camlp5" + +package "grammar" ( + + description = "Coq Camlp5 Grammar Extensions for Plugins" + version = "8.9" + + requires = "camlp5.gramlib" + directory = "grammar" + + archive(byte) = "grammar.cma" + archive(native) = "grammar.cmxa" +) + +package "config" ( + + description = "Coq Configuration Variables" + version = "8.9" + + directory = "config" + +) + +package "clib" ( + description = "Base General Coq Library" + version = "8.9" + + directory = "clib" + requires = "num, str, unix, threads" + + archive(byte) = "clib.cma" + archive(native) = "clib.cmxa" +) + +package "lib" ( + + description = "Base Coq-Specific Library" + version = "8.9" + + directory = "lib" + + requires = "coq.clib, coq.config" + + archive(byte) = "lib.cma" + archive(native) = "lib.cmxa" + +) + +package "vm" ( + + description = "Coq VM" + version = "8.9" + + directory = "kernel/byterun" + +# We could generate this file at configure time for the share byte +# build path to work properly. +# +# Enable this setting for local byte builds if you want dynamic linking: +# +# linkopts(byte) = "-dllpath path_to_coq/kernel/byterun/ -dllib -lcoqrun" + +# We currently prefer static linking of the VM. + archive(byte) = "libcoqrun.a" + linkopts(byte) = "-custom" +) + +package "kernel" ( + + description = "Coq's Kernel" + version = "8.9" + + directory = "kernel" + + requires = "dynlink, coq.lib, coq.vm" + + archive(byte) = "kernel.cma" + archive(native) = "kernel.cmxa" + +) + +package "library" ( + + description = "Coq Libraries (vo) support" + version = "8.9" + + requires = "coq.kernel" + + directory = "library" + + archive(byte) = "library.cma" + archive(native) = "library.cmxa" + +) + +package "engine" ( + + description = "Coq Tactic Engine" + version = "8.9" + + requires = "coq.library" + directory = "engine" + + archive(byte) = "engine.cma" + archive(native) = "engine.cmxa" + +) + +package "pretyping" ( + + description = "Coq Pretyper" + version = "8.9" + + requires = "coq.engine" + directory = "pretyping" + + archive(byte) = "pretyping.cma" + archive(native) = "pretyping.cmxa" + +) + +package "interp" ( + + description = "Coq Term Interpretation" + version = "8.9" + + requires = "coq.pretyping" + directory = "interp" + + archive(byte) = "interp.cma" + archive(native) = "interp.cmxa" + +) + +package "proofs" ( + + description = "Coq Proof Engine" + version = "8.9" + + requires = "coq.interp" + directory = "proofs" + + archive(byte) = "proofs.cma" + archive(native) = "proofs.cmxa" + +) + +package "parsing" ( + + description = "Coq Parsing Engine" + version = "8.9" + + requires = "camlp5.gramlib, coq.proofs" + directory = "parsing" + + archive(byte) = "parsing.cma" + archive(native) = "parsing.cmxa" + +) + +package "printing" ( + + description = "Coq Printing Engine" + version = "8.9" + + requires = "coq.parsing" + directory = "printing" + + archive(byte) = "printing.cma" + archive(native) = "printing.cmxa" + +) + +package "tactics" ( + + description = "Coq Basic Tactics" + version = "8.9" + + requires = "coq.printing" + directory = "tactics" + + archive(byte) = "tactics.cma" + archive(native) = "tactics.cmxa" + +) + +package "vernac" ( + + description = "Coq Vernacular Interpreter" + version = "8.9" + + requires = "coq.tactics" + directory = "vernac" + + archive(byte) = "vernac.cma" + archive(native) = "vernac.cmxa" + +) + +package "stm" ( + + description = "Coq State Transactional Machine" + version = "8.9" + + requires = "coq.vernac" + directory = "stm" + + archive(byte) = "stm.cma" + archive(native) = "stm.cmxa" + +) + +package "toplevel" ( + + description = "Coq Toplevel" + version = "8.9" + + requires = "coq.stm" + directory = "toplevel" + + archive(byte) = "toplevel.cma" + archive(native) = "toplevel.cmxa" + +) + +package "idetop" ( + + description = "Coq IDE Libraries" + version = "8.9" + + requires = "coq.toplevel" + directory = "ide" + + archive(byte) = "coqidetop.cma" + archive(native) = "coqidetop.cmxa" + +) + +# XXX Depends on way less than toplevel +package "ide" ( + + description = "Coq IDE Libraries" + version = "8.9" + +# XXX Add GTK + requires = "coq.toplevel" + directory = "ide" + + archive(byte) = "ide.cma" + archive(native) = "ide.cmxa" + +) + +package "plugins" ( + + description = "Coq built-in plugins" + version = "8.9" + + directory = "plugins" + + package "ltac" ( + + description = "Coq LTAC Plugin" + version = "8.9" + + requires = "coq.stm" + directory = "ltac" + + archive(byte) = "ltac_plugin.cmo" + archive(native) = "ltac_plugin.cmx" + + ) + + package "tauto" ( + + description = "Coq tauto plugin" + version = "8.9" + + requires = "coq.plugins.ltac" + directory = "ltac" + + archive(byte) = "tauto_plugin.cmo" + archive(native) = "tauto_plugin.cmx" + ) + + package "omega" ( + + description = "Coq omega plugin" + version = "8.9" + + requires = "coq.plugins.ltac" + directory = "omega" + + archive(byte) = "omega_plugin.cmo" + archive(native) = "omega_plugin.cmx" + ) + + package "romega" ( + + description = "Coq romega plugin" + version = "8.9" + + requires = "coq.plugins.omega" + directory = "romega" + + archive(byte) = "romega_plugin.cmo" + archive(native) = "romega_plugin.cmx" + ) + + package "micromega" ( + + description = "Coq micromega plugin" + version = "8.9" + + requires = "num,coq.plugins.ltac" + directory = "micromega" + + archive(byte) = "micromega_plugin.cmo" + archive(native) = "micromega_plugin.cmx" + ) + + package "quote" ( + + description = "Coq quote plugin" + version = "8.9" + + requires = "coq.plugins.ltac" + directory = "quote" + + archive(byte) = "quote_plugin.cmo" + archive(native) = "quote_plugin.cmx" + ) + + package "newring" ( + + description = "Coq newring plugin" + version = "8.9" + + requires = "coq.plugins.quote" + directory = "setoid_ring" + + archive(byte) = "newring_plugin.cmo" + archive(native) = "newring_plugin.cmx" + ) + + package "fourier" ( + + description = "Coq fourier plugin" + version = "8.9" + + requires = "coq.plugins.ltac" + directory = "fourier" + + archive(byte) = "fourier_plugin.cmo" + archive(native) = "fourier_plugin.cmx" + ) + + package "extraction" ( + + description = "Coq extraction plugin" + version = "8.9" + + requires = "coq.plugins.ltac" + directory = "extraction" + + archive(byte) = "extraction_plugin.cmo" + archive(native) = "extraction_plugin.cmx" + ) + + package "cc" ( + + description = "Coq cc plugin" + version = "8.9" + + requires = "coq.plugins.ltac" + directory = "cc" + + archive(byte) = "cc_plugin.cmo" + archive(native) = "cc_plugin.cmx" + ) + + package "ground" ( + + description = "Coq ground plugin" + version = "8.9" + + requires = "coq.plugins.ltac" + directory = "firstorder" + + archive(byte) = "ground_plugin.cmo" + archive(native) = "ground_plugin.cmx" + ) + + package "rtauto" ( + + description = "Coq rtauto plugin" + version = "8.9" + + requires = "coq.plugins.ltac" + directory = "rtauto" + + archive(byte) = "rtauto_plugin.cmo" + archive(native) = "rtauto_plugin.cmx" + ) + + package "btauto" ( + + description = "Coq btauto plugin" + version = "8.9" + + requires = "coq.plugins.ltac" + directory = "btauto" + + archive(byte) = "btauto_plugin.cmo" + archive(native) = "btauto_plugin.cmx" + ) + + package "recdef" ( + + description = "Coq recdef plugin" + version = "8.9" + + requires = "coq.plugins.extraction" + directory = "funind" + + archive(byte) = "recdef_plugin.cmo" + archive(native) = "recdef_plugin.cmx" + ) + + package "nsatz" ( + + description = "Coq nsatz plugin" + version = "8.9" + + requires = "num,coq.plugins.ltac" + directory = "nsatz" + + archive(byte) = "nsatz_plugin.cmo" + archive(native) = "nsatz_plugin.cmx" + ) + + package "natsyntax" ( + + description = "Coq natsyntax plugin" + version = "8.9" + + requires = "" + directory = "syntax" + + archive(byte) = "nat_syntax_plugin.cmo" + archive(native) = "nat_syntax_plugin.cmx" + ) + + package "zsyntax" ( + + description = "Coq zsyntax plugin" + version = "8.9" + + requires = "" + directory = "syntax" + + archive(byte) = "z_syntax_plugin.cmo" + archive(native) = "z_syntax_plugin.cmx" + ) + + package "rsyntax" ( + + description = "Coq rsyntax plugin" + version = "8.9" + + requires = "" + directory = "syntax" + + archive(byte) = "r_syntax_plugin.cmo" + archive(native) = "r_syntax_plugin.cmx" + ) + + package "int31syntax" ( + + description = "Coq int31syntax plugin" + version = "8.9" + + requires = "" + directory = "syntax" + + archive(byte) = "int31_syntax_plugin.cmo" + archive(native) = "int31_syntax_plugin.cmx" + ) + + package "asciisyntax" ( + + description = "Coq asciisyntax plugin" + version = "8.9" + + requires = "" + directory = "syntax" + + archive(byte) = "ascii_syntax_plugin.cmo" + archive(native) = "ascii_syntax_plugin.cmx" + ) + + package "stringsyntax" ( + + description = "Coq stringsyntax plugin" + version = "8.9" + + requires = "coq.plugins.asciisyntax" + directory = "syntax" + + archive(byte) = "string_syntax_plugin.cmo" + archive(native) = "string_syntax_plugin.cmx" + ) + + package "derive" ( + + description = "Coq derive plugin" + version = "8.9" + + requires = "" + directory = "derive" + + archive(byte) = "derive_plugin.cmo" + archive(native) = "derive_plugin.cmx" + ) + + package "ssrmatching" ( + + description = "Coq ssrmatching plugin" + version = "8.9" + + requires = "coq.plugins.ltac" + directory = "ssrmatching" + + archive(byte) = "ssrmatching_plugin.cmo" + archive(native) = "ssrmatching_plugin.cmx" + ) + + package "ssreflect" ( + + description = "Coq ssreflect plugin" + version = "8.9" + + requires = "coq.plugins.ssrmatching" + directory = "ssr" + + archive(byte) = "ssreflect_plugin.cmo" + archive(native) = "ssreflect_plugin.cmx" + ) +) diff --git a/Makefile b/Makefile index df5caf0b7..636093d7a 100644 --- a/Makefile +++ b/Makefile @@ -80,7 +80,9 @@ export MLPACKFILES := $(call find, '*.mlpack') export ML4FILES := $(call find, '*.ml4') export MLGFILES := $(call find, '*.mlg') export CFILES := $(call findindir, 'kernel/byterun', '*.c') -export MERLINFILES := $(call find, '.merlin') + +export MERLININFILES := $(call find, '.merlin.in') +export MERLINFILES := $(MERLININFILES:.in=) # NB: The lists of currently existing .ml and .mli files will change # before and after a build or a make clean. Hence we do not export @@ -175,7 +177,7 @@ Makefile $(wildcard Makefile.*) config/Makefile : ; .PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean depclean cleanconfig distclean voclean timingclean devdocclean alienclean -clean: objclean cruftclean depclean docclean devdocclean +clean: objclean cruftclean depclean docclean devdocclean camldevfilesclean cleankeepvo: indepclean clean-ide optclean cruftclean depclean docclean devdocclean @@ -185,6 +187,9 @@ cruftclean: ml4clean find . -name '*~' -o -name '*.annot' | xargs rm -f rm -f gmon.out core +camldevfilesclean: + rm -f $(MERLINFILES) META.coq + indepclean: rm -f $(GENFILES) rm -f $(COQTOPBYTE) $(CHICKENBYTE) $(TOPBYTE) diff --git a/Makefile.build b/Makefile.build index 84f86c99a..b60fff0db 100644 --- a/Makefile.build +++ b/Makefile.build @@ -64,7 +64,7 @@ AFTER ?= # build the different subsystems: -world: coq coqide documentation revision +world: camldevfiles coq coqide documentation revision coq: coqlib coqbinaries tools diff --git a/Makefile.dev b/Makefile.dev index 8f7d21694..59097bd91 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -15,7 +15,7 @@ # Debug printers in dev/ ######################### -.PHONY: devel printers +.PHONY: devel printers camldevfiles DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/checker_printers.cmo @@ -85,13 +85,27 @@ endif # But these partial targets could be quite handy for quick builds # of specific components of Coq. +########################################################################### +# OCaml dev files +########################################################################### +camldevfiles: $(MERLINFILES) META.coq + +.merlin: .merlin.in + cp -a "$<" "$@" + +%/.merlin: %/.merlin.in + cp -a "$<" "$@" + +META.coq: META.coq.in + cp -a "$<" "$@" + ############################### ### 1) general-purpose targets ############################### coqlight: theories-light tools coqbinaries -states: theories/Init/Prelude.vo +states: camldevfiles theories/Init/Prelude.vo miniopt: $(COQTOPEXE) pluginsopt minibyte: $(COQTOPBYTE) pluginsbyte diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el index 70a9756e5..ec72f9650 100644 --- a/dev/tools/coqdev.el +++ b/dev/tools/coqdev.el @@ -33,7 +33,7 @@ (defun coqdev-default-directory () "Return the Coq repository containing `default-directory'." - (let ((dir (locate-dominating-file default-directory "META.coq"))) + (let ((dir (locate-dominating-file default-directory "META.coq.in"))) (when dir (expand-file-name dir)))) (defun coqdev-setup-compile-command () diff --git a/ide/.merlin b/ide/.merlin deleted file mode 100644 index 953b5dce4..000000000 --- a/ide/.merlin +++ /dev/null @@ -1,6 +0,0 @@ -PKG unix laglgtk2 lablgtk2.sourceview2 - -S utils -B utils - -REC diff --git a/ide/.merlin.in b/ide/.merlin.in new file mode 100644 index 000000000..953b5dce4 --- /dev/null +++ b/ide/.merlin.in @@ -0,0 +1,6 @@ +PKG unix laglgtk2 lablgtk2.sourceview2 + +S utils +B utils + +REC diff --git a/plugins/.merlin b/plugins/.merlin deleted file mode 100644 index 2ba616962..000000000 --- a/plugins/.merlin +++ /dev/null @@ -1 +0,0 @@ -REC diff --git a/plugins/.merlin.in b/plugins/.merlin.in new file mode 100644 index 000000000..2ba616962 --- /dev/null +++ b/plugins/.merlin.in @@ -0,0 +1 @@ +REC diff --git a/test-suite/unit-tests/.merlin b/test-suite/unit-tests/.merlin deleted file mode 100644 index b2279de74..000000000 --- a/test-suite/unit-tests/.merlin +++ /dev/null @@ -1,6 +0,0 @@ -REC - -S ** -B ** - -PKG oUnit diff --git a/test-suite/unit-tests/.merlin.in b/test-suite/unit-tests/.merlin.in new file mode 100644 index 000000000..b2279de74 --- /dev/null +++ b/test-suite/unit-tests/.merlin.in @@ -0,0 +1,6 @@ +REC + +S ** +B ** + +PKG oUnit -- cgit v1.2.3