diff options
author | 2008-12-16 13:56:19 +0000 | |
---|---|---|
committer | 2008-12-16 13:56:19 +0000 | |
commit | c215c4429a85a6d73cc1a33041258cacbe4de199 (patch) | |
tree | 4af1be58159858191ab85936ac57bd042853a4ae /contrib/omega | |
parent | a869d74f414ba786c66b8eb7450ff6343ff12ebd (diff) |
Take advantage of natdynlink when available: almost all contribs become loadable plugins
- Any contrib foo leads to contrib/foo/foo_plugin.cmxs (and .cma for bytecode).
- Features that were available without any Require are now loaded systematically
when launching coqtop (see Coqtop.load_initial_plugins):
extraction, jprover, cc, ground, dp, recdef, xml
- The other plugins are loaded when a corresponding Require is done:
quote, ring, field, setoid_ring, omega, romega, micromega, fourier
- I experienced a crash (segfault) while turning subtac into a plugin, so this
one stays statically linked into coqtop for now
- When the ocaml version doesn't support natdynlink, or if "-natdynlink no"
is explicitely given to configure, coqtop is statically linked with all of
the above code as usual. Some messages [Ignore ML file Foo_plugin] may appear.
- How should coqdep handle a "Declare ML Module "foo"" if foo is an archive
and not a ml file ? For now, we suppose that the foo.{cmxs,cma} are at the
same location as the .v during the build, but can be moved later in any place of
the ml loadpath.
This is clearly an experimentation. Feedback most welcome...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11687 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/omega')
-rw-r--r-- | contrib/omega/Omega.v | 1 | ||||
-rw-r--r-- | contrib/omega/OmegaPlugin.v | 11 |
2 files changed, 12 insertions, 0 deletions
diff --git a/contrib/omega/Omega.v b/contrib/omega/Omega.v index 3b427162e..30b945718 100644 --- a/contrib/omega/Omega.v +++ b/contrib/omega/Omega.v @@ -19,6 +19,7 @@ Require Export ZArith_base. Require Export OmegaLemmas. Require Export PreOmega. +Declare ML Module "omega_plugin". Hint Resolve Zle_refl Zplus_comm Zplus_assoc Zmult_comm Zmult_assoc Zplus_0_l Zplus_0_r Zmult_1_l Zplus_opp_l Zplus_opp_r Zmult_plus_distr_l diff --git a/contrib/omega/OmegaPlugin.v b/contrib/omega/OmegaPlugin.v new file mode 100644 index 000000000..21535f0d3 --- /dev/null +++ b/contrib/omega/OmegaPlugin.v @@ -0,0 +1,11 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +Declare ML Module "omega_plugin". |