Skip to content
Permalink

Comparing changes

Choose two branches to see what’s changed or to start a new pull request. If you need to, you can also or learn more about diff comparisons.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also . Learn more about diff comparisons here.
base repository: xavierleroy/coq2html
Failed to load repositories. Confirm that selected base ref is valid, then try again.
Loading
base: master
Choose a base ref
...
head repository: affeldt-aist/coq2html
Failed to load repositories. Confirm that selected head ref is valid, then try again.
Loading
compare: mca2html
Choose a head ref
Able to merge. These branches can be automatically merged.

Commits on Jun 25, 2023

  1. Copy the full SHA
    a486de5 View commit details
  2. Copy the full SHA
    d57546c View commit details

Commits on Oct 27, 2023

  1. Copy the full SHA
    0106592 View commit details
  2. Copy the full SHA
    a74bb0d View commit details
  3. temporary: sample output html

    $ ../coq2html/coq2html -d tmp -base mathcomp -coqlib https://coq.inria.fr/doc/V8.18.0/stdlib/ -external . classical/*.v classical/*.glob
    yoshihiro503 committed Oct 27, 2023
    Copy the full SHA
    cbf68e1 View commit details

Commits on Nov 10, 2023

  1. Copy the full SHA
    272f8f4 View commit details
  2. Copy the full SHA
    c860431 View commit details
  3. Copy the full SHA
    ba1f3d8 View commit details
  4. Merge pull request #1 from yoshihiro503/yoshihiro503-patch-1

    Create deploy_static_site.yml
    yoshihiro503 authored Nov 10, 2023
    Copy the full SHA
    fa5ad71 View commit details
  5. Copy the full SHA
    354a5b0 View commit details
  6. Copy the full SHA
    a50c552 View commit details
  7. Copy the full SHA
    d8a2129 View commit details
  8. fix: fix Makefile

    yoshihiro503 committed Nov 10, 2023
    Copy the full SHA
    1a80df6 View commit details
  9. Copy the full SHA
    e8022e9 View commit details
  10. Copy the full SHA
    37201b8 View commit details
  11. Merge remote-tracking branch 'refs/remotes/origin/yoshihiro503@genera…

    …te_index' into yoshihiro503@generate_index
    yoshihiro503 committed Nov 10, 2023
    Copy the full SHA
    5588874 View commit details
  12. Copy the full SHA
    21159b8 View commit details
  13. Copy the full SHA
    1f9901d View commit details
  14. Copy the full SHA
    1121bb9 View commit details
  15. fix: fix footer

    yoshihiro503 committed Nov 10, 2023
    Copy the full SHA
    e1c8303 View commit details

Commits on Nov 17, 2023

  1. Copy the full SHA
    423c703 View commit details
  2. Copy the full SHA
    ad90479 View commit details
  3. output

    yoshihiro503 committed Nov 17, 2023
    Copy the full SHA
    89142fc View commit details
  4. Copy the full SHA
    0f6ba68 View commit details
  5. Copy the full SHA
    594e865 View commit details
  6. doc: our README

    yoshihiro503 committed Nov 17, 2023
    Copy the full SHA
    7e67b78 View commit details
  7. pages: deploy

    yoshihiro503 committed Nov 17, 2023
    Copy the full SHA
    0f05f85 View commit details

Commits on Nov 24, 2023

  1. Copy the full SHA
    9e7d935 View commit details
  2. Copy the full SHA
    bd5b987 View commit details
  3. Copy the full SHA
    7d69859 View commit details
  4. remove html output

    yoshihiro503 committed Nov 24, 2023
    Copy the full SHA
    c437d57 View commit details
  5. Merge pull request #1 from yoshihiro503/yoshihiro503@generate_index

    Generate index and support markdown mode
    affeldt-aist authored Nov 24, 2023
    Copy the full SHA
    b9e05f7 View commit details
  6. Copy the full SHA
    2d2dd75 View commit details
  7. Copy the full SHA
    24a24ac View commit details
  8. ignore binders

    yoshihiro503 committed Nov 24, 2023
    Copy the full SHA
    177b984 View commit details

Commits on Dec 8, 2023

  1. Copy the full SHA
    a9ee5e5 View commit details
  2. Copy the full SHA
    694b590 View commit details
  3. Copy the full SHA
    293cbc5 View commit details
  4. style: warning class

    yoshihiro503 committed Dec 8, 2023
    Copy the full SHA
    d7b50bc View commit details
  5. Copy the full SHA
    c975f33 View commit details
  6. Copy the full SHA
    ff0e1d2 View commit details

Commits on Dec 15, 2023

  1. fix the link

    yoshihiro503 committed Dec 15, 2023
    Copy the full SHA
    77cc59d View commit details
  2. Copy the full SHA
    d0b9ab8 View commit details
  3. Copy the full SHA
    d7bf07d View commit details
  4. feature: ✨ starting (***markdown or (***md supports markdown synt…

    …ax in normal documentation comments
    yoshihiro503 committed Dec 15, 2023
    Copy the full SHA
    bd54854 View commit details
  5. Copy the full SHA
    a983595 View commit details
  6. Copy the full SHA
    8033651 View commit details
  7. Copy the full SHA
    596bb96 View commit details
  8. Copy the full SHA
    2152c61 View commit details
  9. Copy the full SHA
    d30f4c1 View commit details
Showing with 1,905 additions and 119 deletions.
  1. +33 −0 .github/workflows/build.yml
  2. +68 −0 .github/workflows/deploy_static_site.yml
  3. +6 −0 .gitignore
  4. +21 −4 Makefile
  5. +106 −15 README.md
  6. +69 −0 common.ml
  7. +7 −0 common.mli
  8. +114 −15 coq2html.css
  9. +4 −2 coq2html.footer
  10. +20 −3 coq2html.header
  11. +49 −0 coq2html.js
  12. +312 −80 coq2html.mll
  13. +71 −0 doc/doc.org
  14. BIN doc/overview.jpg
  15. +365 −0 generate_index.ml
  16. +23 −0 generate_index.mli
  17. +6 −0 graphviz.ml
  18. +5 −0 graphviz.mli
  19. +2 −0 ocamldot/LICENSE
  20. +23 −0 ocamldot/Makefile
  21. +34 −0 ocamldot/README
  22. +52 −0 ocamldot/ocamldot.1
  23. +369 −0 ocamldot/ocamldot.mll
  24. +5 −0 range.ml
  25. +7 −0 range.mli
  26. +1 −0 resources.mli
  27. +11 −0 tools/generate-hierarchy-graph.sh
  28. +38 −0 tools/generate-mathcomp-analysis.sh
  29. +66 −0 xrefTable.ml
  30. +18 −0 xrefTable.mli
33 changes: 33 additions & 0 deletions .github/workflows/build.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
name: Builds, tests & co

on:
- push
- pull_request

permissions: read-all

jobs:
build:
strategy:
fail-fast: false
matrix:
os:
- ubuntu-latest
- macos-latest
# - windows-latest
ocaml-compiler:
- 5
- 4.14

runs-on: ${{ matrix.os }}

steps:
- name: Checkout tree
uses: actions/checkout@v4

- name: Set-up OCaml
uses: ocaml/setup-ocaml@v3
with:
ocaml-compiler: ${{ matrix.ocaml-compiler }}

- run: eval $(opam env) && make
68 changes: 68 additions & 0 deletions .github/workflows/deploy_static_site.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,68 @@
on:
push:
# branches: ["mcahtml"]

# Allows you to run this workflow manually from the Actions tab
workflow_dispatch:

# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
permissions:
contents: read
pages: write
id-token: write

# Allow only one concurrent deployment, skipping runs queued between the run in-progress and latest queued.
# However, do NOT cancel in-progress runs as we want to allow these production deployments to complete.
concurrency:
group: "pages"
cancel-in-progress: false

jobs:
generate-deploy:
environment:
name: github-pages
url: ${{ steps.deployment.outputs.page_url }}
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v4

- name: Clone Mathcomp Analysis
uses: actions/checkout@v4
with:
repository: math-comp/analysis
path: analysis

- name: Setup Graphviz
uses: ts-graphviz/setup-graphviz@v2

- name: Set-up OCaml
uses: ocaml/setup-ocaml@v3
with:
ocaml-compiler: 4.14
opam-repositories: |
coq-released: https://coq.inria.fr/opam/released
default: https://github.com/ocaml/opam-repository.git
- name: Setup Coq temporary fix for the Dependency Graph
run: opam install -y coq.8.19.2

- name: Build Mathcomp Analysis
run: cd analysis/ && opam install -y --deps-only . && opam exec -- make all install

- name: Build coq2html
run: opam exec -- make

- run: opam exec -- tools/generate-mathcomp-analysis.sh ${GITHUB_SHA::8}

- name: Setup Pages
uses: actions/configure-pages@v4

- name: Upload artifact
uses: actions/upload-pages-artifact@v3
with:
# Upload entire repository
path: 'html/'
- name: Deploy to GitHub Pages
id: deployment
uses: actions/deploy-pages@v4
6 changes: 6 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
@@ -4,3 +4,9 @@ coq2html
resources.ml
*~
#*#
*.annot

html/

ocamldot/ocamldot
ocamldot/ocamldot.ml
25 changes: 21 additions & 4 deletions Makefile
Original file line number Diff line number Diff line change
@@ -1,8 +1,14 @@
OCAMLOPT=ocamlopt -I +str
OCAMLOPT=ocamlopt -I +str -annot
OCAMLLEX=ocamllex

coq2html: resources.cmx coq2html.cmx
$(OCAMLOPT) -o coq2html str.cmxa resources.cmx coq2html.cmx
GEN_IDX=generate_index

PROJ_OBJS=common.cmx graphviz.cmx range.cmx xrefTable.cmx generate_index.cmx

all: coq2html ocamldot/ocamldot

coq2html: $(PROJ_OBJS:.cmx=.cmi) $(PROJ_OBJS) coq2html.cmx
$(OCAMLOPT) -o coq2html str.cmxa resources.cmx $(PROJ_OBJS) coq2html.cmx

%.cmx: %.ml
$(OCAMLOPT) -c $*.ml
@@ -13,10 +19,12 @@ coq2html: resources.cmx coq2html.cmx
%.ml: %.mll
$(OCAMLLEX) $*.mll

generate_index.cmx: resources.cmx

coq2html.cmx: resources.cmx
resources.cmx: resources.cmi

RESOURCES=header footer css redirect
RESOURCES=header footer css js redirect

resources.ml: $(RESOURCES:%=coq2html.%)
(for i in $(RESOURCES); do \
@@ -30,10 +38,19 @@ clean:
rm -f coq2html
rm -f coq2html.ml resources.ml
rm -f *.o *.cm?
$(MAKE) -C ocamldot/ clean

PREFIX=/usr/local
BINDIR=$(PREFIX)/bin

install:
install coq2html $(BINDIR)/coq2html

depend:
ocamldep *.mli *.ml > .depend

-include .depend

# ocamldot
ocamldot/ocamldot: ocamldot/
$(MAKE) -C ocamldot/ ocamldot
121 changes: 106 additions & 15 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,13 +1,35 @@
# coq2html: an HTML documentation generator for Coq
# (a fork of) coq2html: an HTML documentation generator for Coq

## Overview

coq2html is an HTML documentation generator for Coq source files. It is an alternative to the standard coqdoc documentation generator distributed along with Coq. The major feature of coq2html is its ability to fold proof scripts: in the generated HTML, proof scripts are initially hidden, but can be revealed one by one by clicking on the "Proof" keyword. Here is an example of [folding in action](https://compcert.org/doc/html/compcert.common.Memory.html#Mem.valid_access_dec)
This is a fork of coq2html.

coq2html is an HTML documentation generator for Coq source files. It is an alternative to the standard coqdoc documentation generator distributed along with Coq. The major feature of coq2html is its ability to fold proof scripts: in the generated HTML, proof scripts are initially hidden, but can be revealed one by one by clicking on the "Proof" keyword. Here is an example of [folding in action](https://compcert.org/doc/html/compcert.common.Memory.html#Mem.valid_access_dec).

**Compatibility:** to produce cross-references, coq2html reads `.glob` files produced by Coq. The format of those files sometimes changes between major releases of Coq, thus breaking coq2html. The current version of coq2html is believed to be compatible with Coq 8.6 to 8.19.

This fork extends coq2html with:
* generation of indexes (like coqdoc)
* clickable notations (like coqdoc)
* an option `-Q <dir> <coqdir>`
* Markdown and LaTeX notations in comments
* darkmode
* a sidebar that displays the modules tree
* design for mobile phone (wip)

The motivation for this fork it to provide a better documentation tool for [MathComp-Analysis](https://github.com/math-comp/analysis)
which so far has been relying on a fragile combination of coqdoc and sed scripts.

**History:** coq2html was developed and originally distributed as part of the [CompCert](https://compcert.org/) project when it became clear that the coqdoc of the time was not able to format the CompCert Coq sources the desired way. This is the release of coq2html as a stand-alone tool, independent from CompCert.

**Compatibility:** to produce cross-references, coq2html reads `.glob` files produced by `coqc`. Their format is documented in [documented](https://github.com/coq/coq/blob/master/interp/dumpglob.mli). `.glob` files exists since Coq 7.3 (2002-05) but their format has been changing silently between major releases of Coq; it was first documented officially in 2021. For this reason, coq2html has long been only believed to be compatible with Coq 8.6 to 8.13.

### Examples of documentation generated using this fork of coq2hml:

* [MathComp-Analysis](https://github.com/math-comp/analysis): https://yoshihiro503.github.io/coq2html/
* [Monae](https://yoshihiro503.github.io/coq2html/monae/): https://yoshihiro503.github.io/coq2html/monae/
* [CompCert](https://compcert.org/): https://yoshihiro503.github.io/coq2html/compcert/

## Usage

```
@@ -16,15 +38,39 @@ coq2html is an HTML documentation generator for Coq source files. It is an alte

Summary of options:

Option | Summary
--------------------|----------------------------
`-base` _COQDIR_ | Set the name space for the modules being processed
`-coqlib` _URL_ | Set base URL for Coq standard library
`-d` _DIR_ | Output files to directory _DIR_ (default: current directory)
Option | Summary
---------------------------|----------------------------
`-base` _COQDIR_ | Set the name space for the modules being processed
`-coqlib` _URL_ | Set base URL for Coq standard library
`-d` _DIR_ | Output files to directory _DIR_ (default: current directory)
`-external` _URL_ _COQDIR_ | Set base URL for linking references whose names start with _COQDIR_
`-no-css` | Do not add coq2html.css to the output directory
`-redirect` | Generate redirection files
`-short-names` | Use short, unqualified module names in the output
`-no-css` | Do not add coq2html.css to the output directory
`-redirect` | Generate redirection files
`-short-names` | Use short, unqualified module names in the output
`-title` _TITLE_ | Set the title of the index page
`-Q` _DIR_ _COQDIR_ | Map the directory _DIR_ to correspond to the module name _COQDIR_ (similar to `coqc`)
`-hierarchy-graph` _FILE_ | Show the hierarchy graph of <dot-file> on the index.html (You need Graphviz command line tool)

### Usage example

Let us assume that the project [MathComp-Analysis](https://github.com/math-comp/analysis)
is in the directory `analysis` and that coq2hml is installed in the directory `coq2html`
with the following file hierarchy:
```tree
.
├── coq2html/
└── analysis/
```
Then the following command generates the documentation of MathComp-Analysis:
```console
../coq2html/coq2html \
-title "MathComp-Analysis" \
-d html/ -base mathcomp -Q theories analysis \
-coqlib https://coq.inria.fr/doc/V8.18.0/stdlib/ \
-external https://math-comp.github.io/htmldoc/ mathcomp.ssreflect \
-external https://math-comp.github.io/htmldoc/ mathcomp.algebra \
$(find classical/ theories/ -name "*.v" -or -name "*.glob")
```

### HTML generation

@@ -80,18 +126,46 @@ The cross-references to the Coq standard library use the online version of this
```
for the 8.14.1 version of the standard library.

Using the `-external` option, you can add cross-references to other external libraries whose coqdoc or coq2html-generated documentation is accessible online. For example,
Using the `-external` option, you can add cross-references to other external libraries whose coqdoc or coq2html-generated documentation is accessible online. For example,
```
coq2html -external https://math-comp.github.io/htmldoc_1_12_0 mathcomp ...
```
should produce cross-references to the `mathcomp` library modules. (Warning: untested feature.)

## Markup language for documentation comments
## Special handling of proof scripts

Proof scripts are Coq text (outside comments) that
* starts with `Proof` or `Next Obligation` at the beginning of a line;
* ends with `Qed.` or `Defined.` or `Save.` or `Admitted.` or `Abort.` at the end of a line.

A proof script can start and end on the same line, e.g. `Proof. auto. Qed.`

Proof scripts are formatted in a smaller font and folded by default, leaving only the starting line (`Proof`, etc) visible. Clicking on this first line displays the whole proof script.

The syntax of proof scripts is strict. In particular, after stating a `Theorem` or `Lemma`, it does not work to omit the `Proof` keyword and start the script immediately, nor to abort it immediately with `Admitted.` or `Abort.`. Likewise, the dot `.` must follow `Qed`, `Defined`, etc, without spaces. For example, the following proof scripts won't be properly formatted:
```
Lemma x:...
auto. Qed. (* No "Proof." to mark the beginning of the script. *)
Lemma x:...
Admitted. (* No "Proof." to mark the beginning of the script. *)
Lemma x:...
Proof. auto. Defined . (* Whitespace between "Defined" and "." *)
Documentation comments start with `(** ` (two stars followed by a space) or `(**r ` (two stars, the "r" character, one space).
Lemma x:... Proof. Admitted. (* "Proof" must start a new line. *)
```

## Documentation comments

Documentation comments start with
- `(** ` (two stars followed by a space),
- `(**r ` (two stars, the "r" character, one space), or
- `(**md ` (two stars, the "md" string, one space).
```
(** This is a documentation comment. *)
(**r This is a right-aligned documentation comment. *)
(**md This is a Markdown comment. *)
(* This is a regular comment. *)
```
Regular, non-documentation comments are removed from the HTML output, except within proof scripts, where they are kept as is.
@@ -105,6 +179,24 @@ Documentation comments of the `(**` kind are formatted as described next, then i
| cons (hd: A) (tl: list A). (**r the nonempty list [hd::tl] *)
```

Documentation comments of the `(**md` kind are interpreted as Mardown input with possibly LaTeX mathematical notations (between `$` and `$`) inserted.

In addition, comments formatted as follows (80 characters wide)
```
(**md***************************************************************************)
(* *)
(* Some Mardown + LaTeX comment. *)
(* *)
(*******************************************************************************)
```
are displayed inside a frame.

## Markup language for coq2html

Inside documentation comments that are not Markdown, one can use the following features to improve the rendering of comments.
Many of them are subsumed by the Mardown language available in Mardown + LaTeX documentation comments which
should be preferred when possible.

### Inline Coq text

Within a documentation comment, text within square brackets `[...]` is taken to be Coq text and is formatted in monospace font. You can write `[x + S y]` and will get `x + S y`. Square brackets nest properly, hence `[[x;y]]` gives `[x;y]`.
@@ -150,7 +242,7 @@ Lists start with a dash `-` at the beginning of the line. Subsequent lines star
- [cons h t], also written [h :: t], denoting the nonempty list
with head [h] and tail [t].
If we remove the [nil] case and declare a [CoInductive], we get infinite
If we remove the [nil] case and declare a [CoInductive], we get infinite
streams instead of lists. *)
```
Nested lists are built using two, three or four dashes instead of one:
@@ -192,4 +284,3 @@ Lemma x:... Proof. Admitted. (* "Proof" must start a new line. *)
- All non-ASCII Unicode characters are treated as being parts of identifiers. Hence, `A ⊕ B` is read as three identifiers, `A`, ``, and `B`, and links are correctly added to `A` and `B` if they are bound at top-level. However, `A⊕B` is read as a single identifier, which has no corresponding definition, therefore no link is added.

- The formatting of right-hanging documentation comments `(**r` is inflexible and not appropriate for narrow display windows or long source lines.

Loading