aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc
Commit message (Collapse)AuthorAge
* Merge PR #997: coqdoc: Support comments in verbatim outputGravatar Maxime Dénès2017-09-07
|\
| * coqdoc: Support comments in verbatim outputGravatar Tej Chajed2017-08-29
| | | | | | | | Fixes BZ#5700
* | Fix coqdoc URLs under Windows.Gravatar Théo Zimmermann2017-08-21
|/ | | | URLs on Windows are the same as on Unix, they use / not \.
* Fixing #5648 (too early decision of tagging ident as keyword in html coqdoc).Gravatar Hugo Herbelin2017-07-15
| | | | | | | | | | Fix proposed by the reporter, Vincent Laporte. Note that for LaTeX output, the selection of a keyword was already done after checking if the ident is recognized as a Coq ident by coqtop. Incidentally, being now explicit on an wildcard-catching of exceptions.
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Makefile: no bytecode compilation in make world, see make byte insteadGravatar Pierre Letouzey2017-05-30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | On a machine for which ocamlopt is available, the make world will now perform bytecode compilation only in grammar/ (up to the syntax extension grammar.cma), and then exclusively use ocamlopt. In particular, make world do not build bin/coqtop.byte. A separate rule 'make byte' does it, as well as bytecode plugins and things like dev/printers.cma. 'make install' deals only with the part built by 'make', while a new rule 'make install-byte' installs the part built by 'make byte'. IMPORTANT: PLEASE AVOID doing things like 'make -j world byte' or any parallel mix of native and byte rules. These are known to crash sometimes, see below. Instead, do rather 'make -j && make -j byte'. Indeed, apart from marginal compilation speed-up for users not interested in byte versions, the main reason for this commit is to discourage any simultaneous use of OCaml native and byte compilers. Indeed, ocamlopt and ocamlc will both happily destroy and recreate .cmi for .ml files with no .mli, and in case of parallel build this may happen at the very moment another ocaml(c|opt) is accessing this .cmi. Until now, this issue has been handled via nasty hacks (see the former MLWITHOUTMLI and HACKMLI vars in Makefile.build). But these hacks weren't obvious to extend to ocamlopt -pack vs. ocamlopt -pack. coqdep_boot takes a "-dyndep" option to control precisely how a Declare ML Module influences the .v.d dependency file. Possible values are: -dyndep opt : regular situation now, depends only on .cmxs -dyndep byte : no ocamlopt, or compilation forced to bytecode, depends on .cm(o|a) -dyndep both : earlier behavior, dependency over both .cm(o|a) and .cmxs -dyndep none : interesting for coqtop with statically linked plugins -dyndep var : place Makefile variables $(DYNLIB) and $(DYNOBJ) in .v.d instead of extensions .cm*, so that the choice is made in the rest of the makefile (see a future commit about coq_makefile) NB: two extra mli added to avoid building unecessary .cmo during 'make world', without having to use the ocamldep -native option. NB: we should state somewhere that coqmktop -top won't work unless 'make byte' was done first
* Merge PR#356: Making management of installation directories more structured, ↵Gravatar Maxime Dénès2017-05-30
|\ | | | | | | more uniform
* \ Merge PR#692: Fail on deprecated warning even for Ocaml > 4.02.3Gravatar Maxime Dénès2017-05-30
|\ \
| | * Using the same strategy in coqdoc than in coqtop to guess the coqlib.Gravatar Hugo Herbelin2017-05-29
| | |
| | * Exporting the suffixes needed to build coqlib, docdir, etc.Gravatar Hugo Herbelin2017-05-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | This allows to centralize in the configuration file the description of the 3 possible installation layouts (dispatched over directories shared by multiple application as in unix, self-contained style like in windows, local non-installation as with option -local). Also supporting relocalisation when -prefix or -libdir and co is given.
| | * Using Coq_config.local rather than None to tell that Coq_config.coqlib is local.Gravatar Hugo Herbelin2017-05-29
| |/ |/| | | | | | | This goes towards an approach where a local layout can be seen as an installed layout.
| * Fail on deprecated warning even for Ocaml > 4.02.3Gravatar Gaëtan Gilbert2017-05-28
| | | | | | | | | | | | | | | | Deprecations which can't be fixed in 4.02.3 are locally wrapped with [@@@ocaml.warning "-3"]. The only ones encountered are - capitalize to capitalize_ascii and variants. Changing to ascii would break coqdoc -latin1 and maybe other things though. - external "noalloc" to external [@@noalloc]
* | [coqdoc] Add keywords in bug 2884.Gravatar Emilio Jesus Gallego Arias2017-05-20
|/
* Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
|
* [misc] Remove warnings about String.setGravatar Emilio Jesus Gallego Arias2017-03-20
| | | | | The `a.[i] <- x` notation is deprecated and we were getting a couple of warnings.
* [safe-string] toolsGravatar Emilio Jesus Gallego Arias2017-03-14
| | | | No functional changes.
* Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-08-21
|\
| * Output a break before a list only if there was an empty line (bug #4606).Gravatar Guillaume Melquiond2016-08-16
| | | | | | | | | | | | | | | | | | Moreover, this commit makes sure that an empty line after a list is always translated into a break. ("StartLevel 1" was excluded, for some reason.) It also avoids some code duplication. In particular, "stop_item ()" is defined as "reach_item_level 0", so there is no reason to handle "StartLevel 1" specially.
* | Revert "Merge remote-tracking branch 'github/pr/229' into trunk"Gravatar Maxime Dénès2016-07-05
| | | | | | | | | | | | | | | | | | This reverts commit b2f8f9edd5c1bb0a9c8c4f4b049381b979d3e385, reversing changes made to da99355b4d6de31aec5a660f7afe100190a8e683. Hugo asked for more discussion on this topic, and it was not in the roadmap. I merged it prematurely because I thought there was a consensus. Also, I missed that it was changing coq_makefile. Sorry about that.
* | Makefile: no bytecode compilation in make world, see make byte insteadGravatar Pierre Letouzey2016-06-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | On a machine for which ocamlopt is available, the make world will now perform bytecode compilation only in grammar/ (up to the syntax extension grammar.cma), and then exclusively use ocamlopt. In particular, make world do not build bin/coqtop.byte. A separate rule 'make byte' does it, as well as bytecode plugins and things like dev/printers.cma. 'make install' deals only with the part built by 'make', while a new rule 'make install-byte' installs the part built by 'make byte'. IMPORTANT: PLEASE AVOID doing things like 'make -j world byte' or any parallel mix of native and byte rules. These are known to crash sometimes, see below. Instead, do rather 'make -j && make -j byte'. Indeed, apart from marginal compilation speed-up for users not interested in byte versions, the main reason for this commit is to discourage any simultaneous use of OCaml native and byte compilers. Indeed, ocamlopt and ocamlc will both happily destroy and recreate .cmi for .ml files with no .mli, and in case of parallel build this may happen at the very moment another ocaml(c|opt) is accessing this .cmi. Until now, this issue has been handled via nasty hacks (see the former MLWITHOUTMLI and HACKMLI vars in Makefile.build). But these hacks weren't obvious to extend to ocamlopt -pack vs. ocamlopt -pack. coqdep_boot takes a "-dyndep" option to control precisely how a Declare ML Module influences the .v.d dependency file. Possible values are: -dyndep opt : regular situation now, depends only on .cmxs -dyndep byte : no ocamlopt, or compilation forced to bytecode, depends on .cm(o|a) -dyndep both : earlier behavior, dependency over both .cm(o|a) and .cmxs -dyndep none : interesting for coqtop with statically linked plugins -dyndep var : place Makefile variables $(DYNLIB) and $(DYNOBJ) in .v.d instead of extensions .cm*, so that the choice is made in the rest of the makefile (see next commit about coq_makedile) NB: two extra mli added to avoid building unecessary .cmo during 'make world', without having to use the ocamldep -native option. NB: we should state somewhere that coqmktop -top won't work unless 'make byte' was done first
* | Merge branch 'v8.5' into trunkGravatar Guillaume Melquiond2016-06-03
|\|
| * Fix proof terminators not being detected in presence of curly brackets (bug ↵Gravatar Guillaume Melquiond2016-06-03
| | | | | | | | | | | | #4770). This also fixes comments not being properly skipped when looking for eol.
| * Make "coqdoc -g --parse-comments" behave properly (bug #4773).Gravatar Guillaume Melquiond2016-06-03
| | | | | | | | | | | | As a side effect, there should be a small speedup when ignoring comments. This commit also fixes two bugs related to handling "$$" and "#" in comments.
* | Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
|/
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
|
* Support "Functional Scheme" in coqdoc. (Fix bug #4382)Gravatar Guillaume Melquiond2015-10-23
|
* Documenting how to support some special unicode characters in coqdocGravatar Hugo Herbelin2015-09-26
| | | | (thanks to coq-club, Sep 2015).
* Clarifying the doc of coqdoc --utf8 as discussed on coq-club on August 19, 2015.Gravatar Hugo Herbelin2015-09-26
|
* Remove usage of Printexc.catch in the tools, as it is deprecated since 2001.Gravatar Guillaume Melquiond2015-07-30
| | | | | | | | "This function is deprecated: the runtime system is now able to print uncaught exceptions as precisely as Printexc.catch does. Moreover, calling Printexc.catch makes it harder to track the location of the exception using the debugger or the stack backtrace facility. So, do not use Printexc.catch in new code."
* Avoid outputting stray "Local" keywords in HTML documentation.Gravatar Guillaume Melquiond2015-04-02
|
* Do not escape "'" when outputting to html, especially not using "&acute;".Gravatar Guillaume Melquiond2015-03-31
|
* Make coqdoc -l properly handle Local before Ltac. (Fix for bug #3307)Gravatar Guillaume Melquiond2015-02-11
|
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Improve error recovery in case of ill-formed coqdoc comment. (Fix for bug ↵Gravatar Guillaume Melquiond2015-01-06
| | | | #3802.)
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
|
* coqdoc.css: fix a few errorsGravatar Pierre Letouzey2014-12-09
|
* coqdoc: fix a few issues with xhtml validity (backport 1636f7 and 754abf1 ↵Gravatar Pierre Letouzey2014-12-09
| | | | | | | | | | | | | | | | | from v8.4) - For the style of identifiers, coqdoc was using a 'type' attribute of tag <span>. But this attribute isn't a legal attribute of tag <span> according to the xhtml norm. Instead, I propose to use 'title' for that. The coqdoc.css now supports both approaches. - The names of inner links (cross references #foo) were containing arbitrary characters (in the case of a notation string). For instance in Utf8_core : <a name=":type_scope:'∀'_x_'..'_x_','_x"> Instead, when strange characters are detected, we now hash the string via Digest, and use this hexa hash as html label. - And some whitespace before />
* Port to trunk commit r16062 of v8.4 (Correction des entêtes pour la ↵Gravatar notin2014-12-09
| | | | documentation en ligne)
* Use the url package, since coqdoc generates \url commands.Gravatar Guillaume Melquiond2014-10-27
|
* Supporting Greek and Coptic (U0370) as first letter of coqdoc identifiers.Gravatar Hugo Herbelin2014-10-22
|
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
| | | | Involves changing the [mind_finite] field in the kernel from a bool to the trivalued type [Decl_kinds.recursivity_kind]. This is why so many files are (unfortunately) affected. It would not be very surprising if some bug was introduced.
* Add a [Variant] declaration which allows to write non-recursive variant types.Gravatar Arnaud Spiwack2014-09-04
| | | | Just like the [Record] keyword allows only non-recursive records.
* coqdoc is minimaly -Q awareGravatar Pierre Boutillier2014-07-03
|
* Recognize Parameters as a command in coqdoc. (Fix for bug #3279)Gravatar Guillaume Melquiond2014-04-28
|
* Mark lazymatch as an Ltac keyword for coqdoc. (Fix for bug #3276)Gravatar Guillaume Melquiond2014-04-28
|
* Fixing coqdoc bug #3292 (unfortunate collision betweens the relativeGravatar Hugo Herbelin2014-04-28
| | | | | | | | | locations found when parsing expressions in comments and the absolute locations in the glob file). As now, the glob file does not parse comment, so I removed the test for location when parsing expressions in comments, which anyway are not linkable, precisely because not parsed by coqc.
* Dumpglob: factor out reference dumping.Gravatar Carst Tankink2014-04-10
| | | | | Factored out all functions that dump references to use one function "dump_ref"
* Prevent verbatim text from leaking out of comments. (See bug #2882)Gravatar Guillaume Melquiond2014-04-04
|
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
| | | | | | | | With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment.
* Set officially the minimal OCaml requirement to 3.12.1Gravatar Pierre Letouzey2014-03-02
| | | | | | | | | | | | | | | Anyway, a few syntactic features of 3.12 were already used here and there (e.g. local opening via Foo.(...), or the record shortcut { field; ... }). Hence compiling with 3.11 wasn't working anymore. Already take advantage of the following 3.12.1 features : - "module type of ..." in CArray, CList, CString ... - "ocamldep -ml-synonym" : no need anymore to hack the ocamldep output via our coqdep to localize the .ml4 modules :-) The -ml-synonym option (+ various bugfixes) is the reason for asking 3.12.1 directly and not just 3.12.0. After all, if debian stable is providing 3.12.1, then everybody has it ;-)