| Age | Commit message (Collapse) | Author |
|---|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14035 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
This is to allow users to install plugins when coq is installed system-wide.
Signed-off-by: Tom Prince <tom.prince@ualberta.net>
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14001 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
This allows the construction of an extended library that shadows the standard
library.
Signed-off-by: Tom Prince <tom.prince@ualberta.net>
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14000 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
discipline to files from stdlib or user library
(also factorized code with add_known)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13982 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
coq_makefile uses ocaml{c,opt}.opt if it uses coqc -opt and ocaml‘c,opt}
if it uses coqc -byte.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13980 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13953 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
user-contrib directory.
In particular, this directory should be traversed recursively and the full name of its libraries should not be prefixed by the "Coq" logical path.
This fixes coqdep spamming the following message while the yyy library is in the user-contrib loadpath.
*** Warning: in file xxx.v, library yyy.v is required and has not been found in loadpath!
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13949 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
According to B. Gregoire, this stuff is obsolete. Fine control
on when to launch the VM in conversion problems is now provided
by VMcast. We were already almost never boxing definitions anymore
in stdlib files.
"(Un)Boxed Definition foo" will now trigger a parsing error,
same with Fixpoint. The option "(Un)Set Boxed Definitions"
aren't there anymore, but tolerated (as no-ops), since unknown
options raise a warning instead of an error by default.
Some more cleaning could be done in the vm.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13806 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
symbol).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13691 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
in coqdoc index files).
Bug #2183 was fixed by changing "module" into "moduleid" in Index.type_name
instead of changing "moduleid" into "module". But "moduleid" is used
for building the html indexes what led to not very nice output (one
would expect to see "module" in the index).
Apparently, the reason "moduleid" was used instead of "module" as
internal name for rendering module in the TeX output of coqdoc was
that there were already an old \coqdocmodule historically introduced
by Jean-Christophe to format libraries. But this \coqdocmodule seems
to have been replaced by a \coqlibrary by Matthieu in r11065. So I
conclude that Jean-Christophe's use of \coqdocmodule in coqdoc.sty is
definitively obsolete, that the \coqmodule LaTeX command is free for
other uses and that \coqdocmoduleid has no reason not to be called
\coqdocmodule, and consequently, module has no reason to be some
moduleid in Index.type_name.
Moreover, it remained a \moduleid in Output.module_ref ? Shouldn't it
be \coqdocmoduleid (or actually \coqdocmodule, since the id suffix is
apparently no longer needed).
Hoping I'm not doing something wrong.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13675 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- single quotes in notations were breaking coqdoc, even raising an
out-of-bound error when appearing in the last character of the notation;
- letter "x" in notation tokens were inelegantly surrounded by single quotes,
- rare, but allowed characters < 32 were lost in index pages.
A new fully injective space-free-and-human-readable encoding algorithm
is adopted which put single quotes around all terminal tokens,
double existing single quotes, and replace invisible characters by
^X-like strings.
Moreover, the keywords "Local"/"Global" were blocking the detection of
keywords starting coq lines (e.g. "Local Notation" was not recognized
as a notation). "Local" and "Global" are now uniformly treated as
modifiers of vernac commands as they are in the Coq parser.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13673 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
ability to format inference rules (delimited by [[[ ]]]) and adds some
new flags. Here's the message from Chris:
- coqdoc now has support for inference rules inside coqdoc comments.
These should be enclosed in triple square brackets with the
following format.
[[[
|- t1 : Bool
|- t2 : T |- t3 : T
---------------------------- (T_If)
|- if t1 then t2 else t3 : T
]]]
The rule's name is optional. Multiple inference rules may be
included in the same [[[ ]]] block, separated by blank lines.
See http://www.cis.upenn.edu/~bcpierce/sf/Stlc.html#lab469
for some examples of the output. The output will only be pretty
in html - in other formats it is printed verbatim (though it
shouldn't be hard to add latex support, and I may soon).
- Two new coqdoc flags have been added. First, --inline-notmono
causes inline code to be printed in a proportional width font
(adjustable in the css file). Second, --no-glob tells coqdoc not to
look for .glob files (no links will be inserted for identifiers when
this flag is used).
- Finally, the handling of paragraphs and whitespace around lists
has been made somewhat saner.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13473 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13472 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
this lacks robustness since "coqdoc -g" will drop away any commands unknown
from coqdoc, leading to possible synchronisation problems.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13440 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
coqdep since it is now deterministic (later -R's overwriting former ones).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13432 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- modules names can include quote '
- errors when parsing .mllib files are now properly reported
instead of dying ugly on some sort of Failure
- same when coqdep has to parse the output of ocamldep -modules
- lib/lib.mllib contains a typo (lowercase ident)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13423 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13319 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
If you want to try, it should be now as simple as:
make clean && ./configure -local -usecamlp4 && make
For the moment, the default stays camlp5, hence
./configure -usecamlp5 and ./configure are equivalent.
Thanks to a suggestion by N. Pouillard, the remaining
incompatibilities are now handled via some token filtering in
camlp4. See compat5*.mlp. Morally, these files should be named .ml4,
but I prefer having them not in $(...ML4) variables, it might confuse
the Makefile... The empty compat5*.ml are used to build empty .cmo
for making camlp5 happy. For camlp4,
- tools/compat5.cmo changes GEXTEND into EXTEND. Safe, always loaded
- tools/compat5b.cmo changes EXTEND into EXTEND Gram. Interact badly with
syntax such that VERNAC EXTEND, we only load it for a few files via
camlp4deps
TODO: check that my quick adaptation of camlp5-specific code in
tactics/extratactics.ml4 is ok. It seems the code by Chung-Kil Hur
is hiding information in the locations ?!
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13274 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Looking at the source code of Sys.time reveals that it is exactly what
is computed by Profile.get_time. This can also be tested by evaluating:
Sys.time () -. Unix.(let x = times () in x.tms_utime +. x.tms_stime);;
in an OCaml toplevel with Unix.
This allows to put Profile in grammar.cma without the dependency to
unix.cma while preprocessing.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13233 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13060 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
The choice between camlp4/5 is done during configure with flags
-usecamlp5 (default for the moment) vs. -usecamlp4.
Currently, to have a full camlp4 compatibility, you need to change
all "EXTEND" and "GEXTEND Gram" into "EXTEND Gram", and change "EOI"
into "`EOI" in grammar entries. I've a sed script that does that
(actually the converse), but I prefer to re-think it and check a few
things before branching this sed into the build mechanism.
lib/compat.ml4 is heavily used to hide incompatibilities between camlp4/5
and try to propose a common interface (cf LexerSig / GrammarSig).
A few incompatible quotations have been turned into underlying code
manually, in order to make the IFDEF CAMLP5 THEN ... ELSE ... END
parsable by both camlp4 and 5. See in particular the fate of
<:str_item< declare ... end >>
Stdpp isn't used anymore, but rather Ploc (hidden behind local module Loc).
This forces to use camlp5 > 5.01.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13019 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
These declarations (e.g. make -C .. bin/coqtop.byte) are quite
annoying when debugging stuff over the whole archive: all of a
sudden, M-x recompile isn't doing what you intended just because
you've visited some specific files. Instead:
- Feel free to rather add intermediate targets in the Makefile if
they aren't there yet.
- For avoiding typing the -C with many .. after, you can have a
look at my recursively-descending make:
http://www.pps.jussieu.fr/~letouzey/download/make.sh
which is to be renamed make and placed in a bin dir with more
priority than /usr/bin. Beware! I've already add a few bad surprises
with this hack, but it's really convenient nonetheless.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13014 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Many of them were broken, some of them after Pierre B's rework
of mli for ocamldoc, but not only (many bad annotation, many files
with no svn property about Id, etc)
- Useless for those of us that work with git-svn (and a fortiori
in a forthcoming git-only setting)
- Even in svn, they seem to be of little interest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Made resolution of clashing -I options consistent with coqc (bug #2242)
- Made semantics of -R consistent with the one introduced by revision 11188
in coqc, i.e. -R now makes visible all intermediate qualification levels
(bug #2274)
- Added support for -I -as and -R -as syntax
- Extended escaping of special chars of GNU make and used escaping
more systematically (bug #2118)
- Made warnings follow English typography
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12916 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
rules (bug report #2293).
Restored the sequential extension of the printing rules tables (that
commit #12905 replaced by a per-file modification of the printing
rules table). Note however that the table grows in the order of
compilation of files by coqdoc, which does not necessarily coincide
with the order of coqc compilation dependencies of the files.
Added documentation of coqdoc option "--external".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12908 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
In the initial model (formerly to r11432), coqdoc parsed separatedly
letters and symbolic characters and was thus not able to translate
tokens mixing letters and symbolic characters such as "\in" or "=_h".
Revision 11432 extended the definition of translatable tokens by
supporting letters in it with the benefit of supporting "\in" or "=_h"
but added the constraint of requiring spaces to correctly separate
tokens in expressions such as "x : nat" which otherwise would be split
into "x" and ":nat", then leading to fail understanding "nat" as a
proper reference.
The new model renounces to define a lexical category of tokens and
uses instead a dynamically extensible sublexer similar to the one used
in the Coq lexer. The new model works even if tokens are not separated
by spaces in the source file and it thus solves problems such as the
one mentioned in bug #2273 (failure to link C in "`(!C)"). However, it
imposes a stronger discipline in writing the lexing rules in
cpretty.mll because the characters that can eventually contribute to
the application of a printing rule are buffered in the sublexer and no
output is allowed to occur until the buffer of the sublexer if
flushed.
The theoretical overhead due to the intermediate use of buffers is
apparently less than 5%. More details on the token cutting discipline
can be found in the new file token.mli.
Incidentally fixed two small problems with notation links in LaTeX:
made escaping of characters in LaTeX labels more robust so that
notations do not easily get the same label name; avoid only
highlighting the first '"' of a notation def (failing to have now a
better highlighting strategy).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12905 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
In coqdoc, made links to utf8 notations working and made
representation of locations for notations more compact
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12896 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(it interfered badly with utf-8: just take an utf-8 like "forall" which
starts in iso-8859-1 with a "a circonflex"; nothing is lost since
intentedly iso-8859-1 chars can only occur in comments and there is no
ident detection in comments)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12895 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Local Definitions were considered Global Definitions in globalization file
(bug #2288) [I made them "var" which makes them indexed like
Variables, should we have an extra category just for Let's?]
- the syntax of "[[" was not properly enforced in parse-comments mode
- improved documentation of a few vernac file of the library
- fixed a bug in Makefile.doc leading to build a bigger and bigger
Library.pdf file
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12894 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
from a incorrect computation of logical names + bug in rendering of
name-based notations, aka abbreviations or syntactic definitions).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12893 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- make links to section variables working (used qualified names for
disambiguation and fixed the place in intern_var where to dump them)
(wish #2277)
- mapping of physical to logical paths now follows coq (see bug #2274)
(incidentally, it was also incorrectly seeing foobar.v as a in directory foo)
- added links for notations
- added new category "other" for indexing entries not starting with latin letter
(e.g. notations or non-latin identifiers which was otherwise broken)
- protected non-notation strings (from String.v) from utf8 symbol interpretation
- incidentally quoted parseable _ in notations to avoid confusion with
placeholder in the "_ + _" form of notation
- improved several "Sys_error" error messages
- fixed old bug about second dot of ".." being interpreted as regular dot
- removed obsolete lexer in index.mll (and renamed index.mll to index.ml)
- added a test-suite file for testing various features of coqdoc
Things that still do not work:
- when a notation is redefined several times in the same scope, only
the link to the first definition works
- if chars and symbols are not separated in advance, idents
that immediately follow symbols are not detected
(e.g. as in {True}+{True} where coqdoc sees a symbol "+{True}")
- parentheses, curly brackets and semi-colon not linked in notations
Things that can probably be improved:
- all notations are indexed in the same category "other"; can we do better?
- all non-latin identifiers (e.g. Greek letters) are also indexed in the
same "other" category; can we do better?
- globalization data for notations could be compacted (currently there is one
line per each proper location covered by the notation)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12890 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12847 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
When we emulate ocamldep via "coqdep_boot -mldep ocamldep", it's nicer
to get something as output, even if there's no dependencies. Something like
foo.cmo:
foo.cmx:
at least indicates that something has been done. Moreover it's closer to
the behavior of ocamldep
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12838 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- This way, the Makefile.build gets shorter and simplier, with a few nasty
hacks removed.
- In particular, we stop creating dummy .ml of .ml4 early "to please ocamldep".
Instead, we now use ocamldep -modules, and process its output via coqdep_boot.
This ways, *.cm* of .ml4 are correctly located, even when some .ml files
aren't generated yet.
- There is no risk of editing the .ml of a .ml4 by mistake, since it is by
default in a binary format (cf pr_o.cmo and variable READABLE_ML4).
M-x next-error still open the right .ml4 at the right location.
- mltop.byteml is now mltop.ml, while mltop.optml keeps its name
- .ml of .ml4 are added to .gitignore
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12833 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12698 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12696 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12695 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12677 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Class" too to handle references instead of just idents. Minor fix in
coqdoc. zeta-normalize setoid_rewrite proofs, removing useless
let-bindings generated by the tactic.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12609 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
avoiding the introduction of eta-redexes. Prioritize hints over intros
in typeclass resolution to profit from that.
Add a minor fix in coqdoc by F. Garillot.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12550 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12536 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
versions de OCaml antérieures à 3.11.0)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12512 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12492 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Correct backtracking function of coqdoc to handle the _p fields of lexers
- Try a better typesetting of [[ ]] inline code considering it as
blocks and not purely inline code like [ ] escapings.
- Rework latex macros for better factorization and support external
references in pdf output.
- Better criterion for generalization of variables in dependent
elimination tactic and better error message in [specialize_hypothesis].
- In autounfold, don't put the core unfolds by default.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12474 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12469 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12465 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12447 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
branch
and remove equations stuff which moves to a separate plugin.
Classes:
- Ability to define classes post-hoc from constants or inductive types.
- Correctly rebuild the hint database associated to local hypotheses when
they are changed by a [Hint Extern] in typeclass resolution.
Tactics and proofs:
- Change [revert] so that it keeps let-ins (but not [generalize]).
- Various improvements to the [generalize_eqs] tactic to make it more robust
and produce the smallest proof terms possible.
Move [specialize_hypothesis] in tactics.ml as it goes hand in hand with
[generalize_eqs].
- A few new general purpose tactics in Program.Tactics like [revert_until]
- Make transitive closure well-foundedness proofs transparent.
- More uniform testing for metas/evars in pretyping/unification.ml
(might introduce a few changes in the contribs).
Program:
- Better sorting of dependencies in obligations.
- Ability to start a Program definition from just a type and no obligations,
automatically adding an obligation for this type.
- In compilation of Program's well-founded definitions, make the functional a
separate definition for easier reasoning.
- Add a hint database for every Program populated by [Hint Unfold]s for
every defined obligation constant.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12440 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
variables with syntax:
[Local?|Global] Generalizable Variable(s)? [all|none|id1 idn].
By default no variable is generalizable, so this patch breaks backward
compatibility with files that used implicit generalization (through
Instance declarations for example). To get back the old behavior, one
just needs to use [Global Generalizable Variables all].
Make coq_makefile more robust using [mkdir -p].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12428 85f007b7-540e-0410-9357-904b9bb8a0f7
|
