aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
Commit message (Collapse)AuthorAge
...
* Added Add LoadPath in coqdep lexer (but not in coqdep itself by lack of time).Gravatar herbelin2011-10-29
| | | | | | | | | | | | | | | | | | | There are preliminary problems to solve in the semantics of -I/-R which differs from the one of coqtop: - in case of ambiguity, internally to -R option, or between two -R/-I options, it is not clear at all that the semantics is as in coqtop (which by the way is not canonical either since it seems to depend on the underlying order of dirs in the file system), - in the presence of -I dir, Require A.b does not look if dir.A.b exists; similarly for Declare ML Module "f", Require "f" and Load "f" when f has a dirname part. I suggest to have a common library for coqdep, coqdoc and coqtop that ensures that -I/-R behave consistently for all tools. Incidentally made coqdep lexer a bit more strict about syntax errors. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14626 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed broken globalization of identifiers containing utf8 lettersGravatar herbelin2011-10-29
| | | | | | | | | | | | | | | | | | without knowing it. Note: location tables have grown a lot, a better representation of the contents of the glob files in coqdoc might improve efficiency. Also added keywords. Information is now obtained from the glob file to know the exact span of identifiers. Kept a class of identifiers (and enriched them) for the main purpose of distinguishing between idents and symbols in the absence of a glob file. Still a lot of work to do in coqdoc to make it more robust... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14624 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added checksums to glob files and warned about possibly missingGravatar herbelin2011-10-29
| | | | | | packages for utf8. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14623 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq_makefile handles .mlpack filesGravatar pboutill2011-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14617 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqdep handles .mlpackGravatar pboutill2011-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14616 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq_makefile includes coqtop -config without file generationGravatar pboutill2011-10-26
| | | | | | Make the compilation log cleaner. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14609 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq_makefile: libraries in bytecode are now installed tooGravatar pboutill2011-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14608 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq_makefile: a more complete commentary about global variablesGravatar pboutill2011-10-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14599 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq_makefile does not install/compile explicitely cmo and cmxs? that are in ↵Gravatar pboutill2011-10-25
| | | | | | a cmx?a git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14598 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqdep defines a makefile variable name_MLLIB_DEPENDENCIES to store ↵Gravatar pboutill2011-10-25
| | | | | | dependencies of name.mllib git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14597 85f007b7-540e-0410-9357-904b9bb8a0f7
* In Coq_config: get rid of coqsrc and make coqlib optionalGravatar glondu2011-09-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | I assume that once Coq is installed in non-local mode and run from its installed path, sources are no longer available. The coqsrc variable doesn't make any sense, then, and its intended value can always be inferred from Sys.executable_name. Moving it to Envars.coqroot. Make coqlib optional. Currently, it is set to None only in -local mode or with ocamlbuild. When set to None, -local layout is assumed (binaries in ./bin, library in .). The behaviour should not be changed when an explicit coqlib has been given to ./configure. This commit should make it possible to run a Coq compiled with -local from anywhere (no hard-coded absolute path embedded in the executables, intermediary step to bug #2565). It WILL BREAK settings re-using source trees after installation in non-local mode (are there actual use cases for that?). Hard-coded absolute paths still remain: - in the build system, so the need to re-run ./configure after moving the source tree is still expected for now; - in coqrunbyteflags, I think we are limited by ocaml itself; - docdir. All absolute paths should be removed, ultimately. As a side-effect, simplify computing of Envars.coqbin. I don't see any good reason to keep it as a function. Disclaimers: - initialization of Sys.executable_name is not consistent across all architectures; relying so much on it might trigger bugs. I'm pretty sure something will explode if one adds arbitrary symlinks on top of that; - ocamlbuild stuff not tested. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14500 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug #2606 (bad coqdoc processing of coq escaped in comments).Gravatar herbelin2011-09-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14482 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix test-suite/ide for repository compiled without -local (fix #2600)Gravatar letouzey2011-09-19
| | | | | | | | | | | | | | - Add option -boot to the coqtop given to fake_ide - Be sure that a dying coqtop subprocess cannot go unnoticed. Before that, for repositories compiled without -local, coqtop -ideslave was dying immediately because it was missing its coqlib informations. Then the first command send via Marshal.to_channel was triggering a SIGPIPE and hence the death of fake_ide. Strangely, the return code was not necessarily understood as non-zero (?!). We now catch SIGPIPE and do an "exit 1". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14480 85f007b7-540e-0410-9357-904b9bb8a0f7
* avoid dependency nightmare by creating coqdep_{lexer,common}.mliGravatar letouzey2011-09-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* fake_ide: a short program to mimic an ide talking to coqtop -ideslaveGravatar letouzey2011-09-05
| | | | | | | | This way, we can test each night that coqtop -ideslave handles correctly some specific sequences of API calls. For the moment, we add a few tests of the backtracking. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14456 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq_makefile: bugfix in install ruleGravatar pboutill2011-09-02
| | | | | | Files in a -I path are now installed in every root directory of -R pathes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14445 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq_makefile : bug when a project file is not in the current directory.Gravatar pboutill2011-09-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14443 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq_makefile.absolute_dir -> Minilib.canonical_path_nameGravatar pboutill2011-09-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14434 85f007b7-540e-0410-9357-904b9bb8a0f7
* Creation of ide/project_file.ml4Gravatar pboutill2011-09-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14433 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq_makefile: Bug fix of check_depGravatar pboutill2011-09-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14431 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq_makefile: process_cmd_line is purely functional.Gravatar pboutill2011-09-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14430 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq_makefile: No other function than split_arguments uses a target type.Gravatar pboutill2011-09-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14429 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq_makefile: New option -arg to specify a compiler option.Gravatar pboutill2011-09-01
| | | | | | Consequently, option -impredicative-set is deprecated. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14428 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq_makefile drops the '/' at the end of physical path of -I and -RGravatar pboutill2011-09-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14427 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allow custom targets without commands specifiedGravatar pboutill2011-07-22
| | | | | | | | | | | | | | $ coq_makefile -custom "" "install2" "install" for instance does: install: install2 If you tried to do this before, coq_makefile used to insert a TAB after the rule. Signed-off-by: Paolo Herms <paolo.herms@cea.fr> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14290 85f007b7-540e-0410-9357-904b9bb8a0f7
* This adds two option tables 'Printing Record' and 'Printing Constructor'Gravatar herbelin2011-07-16
| | | | | | | | | | | that forces a given type to always be printed as a record, or with a constructor, regardless of the setting of 'Printing Records'. And this is that patch that controls printing by type. (patch from Tom Prince) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14286 85f007b7-540e-0410-9357-904b9bb8a0f7
* This option disables the use of the '{| field := ... |}' notationGravatar herbelin2011-07-16
| | | | | | | | when printing. Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14284 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefiles generated by coq_makefile can build %.cmx?a from %.mllibGravatar pboutill2011-07-11
| | | | | | | A problem remains with the "install" rule because every cmo/cmx is installed even if installing only the generated cma/cmxa could be sufficient. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14275 85f007b7-540e-0410-9357-904b9bb8a0f7
* coq_makefile logical path ending with '.' are correctly convert to physical pathGravatar pboutill2011-07-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14272 85f007b7-540e-0410-9357-904b9bb8a0f7
* coq_makefile bug fix 2405: cmxs are now made from cmx filesGravatar pboutill2011-07-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14271 85f007b7-540e-0410-9357-904b9bb8a0f7
* coq_makefile documentation in Refman and -hGravatar pboutill2011-07-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14270 85f007b7-540e-0410-9357-904b9bb8a0f7
* coq_makefile doesn't complain anymore when a dir is both -I and -RGravatar pboutill2011-07-07
| | | | | | It used to deal correctly with that so why a warning ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14269 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo.Gravatar gmelquio2011-06-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14162 85f007b7-540e-0410-9357-904b9bb8a0f7
* when -camlbin is explicitly given in configure, $OCAML* are $CAMLBIN/exec.Gravatar pboutill2011-04-29
| | | | | | | Coq_makefile wrote $CAMLBIN twice... This should fix ssreflect in bench. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14088 85f007b7-540e-0410-9357-904b9bb8a0f7
* coq_makefile big cleanupGravatar pboutill2011-04-28
| | | | | | | | | | | | | For everybody: variable customization should be easier. (Bug 2533 & more) For plugins: mli files are accepted, doc of them is done, ml4 files really work, ml files aren't camlp* preprocced, ready to build with camlp4 is your code is ready too, should work on any architecture nevermind the one on which you've done the coq_makefile. For others: html doc installation in $DOCDIR/users-contrib/"you"/ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14081 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix for handling of -R "" in coqdoc (bug #2423).Gravatar herbelin2011-04-25
| | | | | | (submitted by Tom Prince <tom.prince@ualberta.net>) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14063 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ocamlbuild: in win32, coqide is now a console-free app by defaultGravatar letouzey2011-04-21
| | | | | | | | | | | | | | This is an adaptation of commit 13748 in 8.3 branch Making coqide console-free can be done via a link flag given to mingw. In case of problem with this setting, I also include a script mkwinapp.ml borrowed from project OCaml-Win32 (and slightly modified to allow restoring the console as well as removing it). Use: "mkwinapp coqide.exe" to make it console-free. "mkwinapp -unset coqide.exe" to go back to usual console app. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14039 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqdoc: also try coqlib relative to the coqdoc binary locationGravatar letouzey2011-04-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14035 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add directories in COQPATH to search path.Gravatar herbelin2011-04-14
| | | | | | | | 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
* Reorder search path order, so the standard library is search last.Gravatar herbelin2011-04-14
| | | | | | | | | 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
* Applying Tom Prince's patch to coqdep not correctly applying the -R visibilityGravatar herbelin2011-04-08
| | | | | | | 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
* A kind of reply to bug 2444Gravatar pboutill2011-04-08
| | | | | | | 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
* Fix last commit about coqdep: not everyone has a user-contrib dirGravatar letouzey2011-04-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13953 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adjust coqdep so that it behaves like coqtop with respect to the ↵Gravatar gmelquio2011-04-01
| | | | | | | | | | 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
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
| | | | | | | | | | | | | | | | 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
* Fixed status of ÷ and × in coqdoc (they were seen as letter instead of ↵Gravatar herbelin2010-12-06
| | | | | | symbol). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13691 85f007b7-540e-0410-9357-904b9bb8a0f7
* Better fix to bug #2183 ("moduleid" internal name got exposed to usersGravatar herbelin2010-12-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* Fixing several bugs with links to notation in coqdoc, including bug #2445:Gravatar herbelin2010-12-04
| | | | | | | | | | | | | | | | | | - 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
* Coqdoc patches from UPenn (thanks to C. Casinghino). This introduces theGravatar msozeau2010-09-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* Minor fixes of 'make doc'Gravatar pboutill2010-09-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13472 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 01:36:49 +0000