Skip to content

Commit a47ce03

Browse files
committed
restructure: coqdoc on master branch
1 parent ac5f1df commit a47ce03

File tree

372 files changed

+65314
-167
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

372 files changed

+65314
-167
lines changed

.circleci/config.yml

Lines changed: 42 additions & 130 deletions
Original file line numberDiff line numberDiff line change
@@ -1,161 +1,73 @@
11
version: 2.1
22

3-
defaults: &defaults
4-
environment:
5-
OPAMBESTEFFORT: true
6-
OPAMJOBS: 2
7-
OPAMVERBOSE: 1
8-
OPAMWITHTEST: true
9-
OPAMYES: true
10-
TERM: xterm
11-
resource_class: medium
12-
13-
commands:
14-
startup:
3+
jobs:
4+
build:
5+
parameters:
6+
coq:
7+
type: string
8+
docker:
9+
- image: coqorg/coq:<<parameters.coq>>
10+
resource_class: medium
11+
environment:
12+
OPAMJOBS: 2
13+
OPAMVERBOSE: 1
14+
OPAMYES: true
15+
TERM: xterm
1516
steps:
1617
- checkout
1718
- run:
1819
name: Pull submodules
19-
command: git submodule update --init --remote
20+
command: git submodule update --init
2021
- run:
2122
name: Configure environment
2223
command: echo . ~/.profile >> $BASH_ENV
2324
- run:
2425
name: Install dependencies
2526
command: |
26-
opam repo -a add coq-extra-dev https://coq.inria.fr/opam/extra-dev
27+
opam repo -a --set-default add coq-extra-dev https://coq.inria.fr/opam/extra-dev
2728
opam update
2829
opam install --deps-only .
2930
- run:
3031
name: List installed packages
3132
command: opam list
32-
build:
33-
steps:
3433
- run:
3534
name: Build, test, and install package
36-
command: opam install .
35+
command: opam install -t .
36+
- run:
37+
name: Generate Coqdoc
38+
command: |
39+
make -j`nproc` html
40+
tar cfz coqdoc.tgz html
41+
- store_artifacts:
42+
path: coqdoc.tgz
3743
- run:
3844
name: Test dependants
3945
command: |
40-
PINS=$(echo `opam list -s --pinned --columns=package` | sed 's/ /,/g')
46+
PINS=$(opam list -s --pinned --columns=package | xargs | tr ' ' ,)
4147
PACKAGES=`opam list -s --depends-on coq-ext-lib --coinstallable-with $PINS`
42-
if ! [ -z "$PACKAGES" ]
43-
then opam install $PACKAGES
48+
if [ -n "$PACKAGES" ]
49+
then opam install -t $PACKAGES
4450
fi
4551
- run:
4652
name: Uninstall package
4753
command: opam uninstall .
48-
- run:
49-
name: Build and test locally
50-
command: make -j`nproc`
51-
- run:
52-
name: Cleanup local directory
53-
command: |
54-
make -j`nproc` clean
55-
ls -AGR
56-
deploy:
57-
steps:
58-
- run:
59-
name: Build Documentation
60-
command: make -j`nproc` html
61-
- run:
62-
name: Configure Git
63-
command: |
64-
git config --global core.autocrlf input
65-
git config --global user.name "Yishuai Li"
66-
git config --global user.email "[email protected]"
67-
- run:
68-
name: Deploy GitHub Pages
69-
command: |
70-
if [ -z "$CIRCLE_TAG" ]
71-
then TAG=$CIRCLE_BRANCH
72-
else TAG=$CIRCLE_TAG
73-
fi
74-
PAGES=$CIRCLE_PROJECT_REPONAME/$TAG
75-
if [ -z "$CIRCLE_PULL_REQUESTS" ]
76-
then git clone -b gh-pages --depth 1 $CIRCLE_REPOSITORY_URL
77-
rm -rf $PAGES/*
78-
mkdir -p $PAGES
79-
cp -LRf html/* $PAGES
80-
cd $CIRCLE_PROJECT_REPONAME
81-
git add .
82-
git commit -m "$TAG $CIRCLE_SHA1" || true
83-
git push
84-
fi
85-
86-
jobs:
87-
coq 8_8:
88-
<<: *defaults
89-
steps:
90-
- startup
91-
- build
92-
docker:
93-
- image: coqorg/coq:8.8
94-
coq 8_9:
95-
<<: *defaults
96-
steps:
97-
- startup
98-
- build
99-
docker:
100-
- image: coqorg/coq:8.9
101-
coq 8_10:
102-
<<: *defaults
103-
steps:
104-
- startup
105-
- build
106-
docker:
107-
- image: coqorg/coq:8.10
108-
coq dev:
109-
<<: *defaults
110-
steps:
111-
- startup
112-
- build
113-
docker:
114-
- image: coqorg/coq:dev
115-
doc:
116-
<<: *defaults
117-
steps:
118-
- startup
119-
- deploy
120-
docker:
121-
- image: coqorg/coq
12254

12355
workflows:
12456
version: 2
125-
build:
57+
test:
12658
jobs:
127-
- coq 8_8:
128-
filters:
129-
branches:
130-
ignore: gh-pages
131-
tags:
132-
only: /^v.*/
133-
- coq 8_9:
134-
filters:
135-
branches:
136-
ignore: gh-pages
137-
tags:
138-
only: /^v.*/
139-
- coq 8_10:
140-
filters:
141-
branches:
142-
ignore: gh-pages
143-
tags:
144-
only: /^v.*/
145-
- coq dev:
146-
filters:
147-
branches:
148-
ignore: gh-pages
149-
tags:
150-
only: /^v.*/
151-
- doc:
152-
requires:
153-
- coq 8_8
154-
- coq 8_9
155-
- coq 8_10
156-
- coq dev
157-
filters:
158-
branches:
159-
ignore: gh-pages
160-
tags:
161-
only: /^v.*/
59+
- build:
60+
name: "Coq 8.8"
61+
coq: "8.8"
62+
- build:
63+
name: "Coq 8.9"
64+
coq: "8.9"
65+
- build:
66+
name: "Coq 8.10"
67+
coq: "8.10"
68+
- build:
69+
name: "Coq 8.11"
70+
coq: "8.11"
71+
- build:
72+
name: "Coq dev"
73+
coq: "dev"

.gitignore

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ deps.pdf
1818
.coqdeps.d
1919
.DS_Store
2020
html
21+
index.md
2122
*.coq.d
2223
*.vok
2324
*.vos

.gitmodules

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,3 @@
11
[submodule "coqdocjs"]
2-
path = coqdocjs
2+
path = docs/coqdocjs
33
url = https://github.com/coq-community/coqdocjs.git
4-
[submodule "templates"]
5-
path = templates
6-
url = https://github.com/coq-ext-lib/templates.git

Makefile

Lines changed: 17 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -1,35 +1,36 @@
11
all: theories examples
22

3-
theories: Makefile.coq
4-
$(MAKE) -f Makefile.coq
3+
include coqdocjs/Makefile.doc
54

6-
Makefile.coq:
7-
$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
5+
theories: $(COQMAKEFILE)
6+
$(MAKE) -f $(COQMAKEFILE)
87

9-
install: Makefile.coq
10-
$(MAKE) -f Makefile.coq install
8+
$(COQMAKEFILE):
9+
$(COQBIN)coq_makefile -f _CoqProject -o $(COQMAKEFILE)
10+
11+
install: $(COQMAKEFILE)
12+
$(MAKE) -f $(COQMAKEFILE) install
1113

1214
examples: theories
1315
$(MAKE) -C examples
1416

1517
clean:
16-
if [ -e Makefile.coq ] ; then $(MAKE) -f Makefile.coq cleanall ; fi
18+
if [ -e $(COQMAKEFILE) ] ; then $(MAKE) -f $(COQMAKEFILE) cleanall ; fi
1719
$(MAKE) -C examples clean
18-
@rm -f Makefile.coq Makefile.coq.conf
20+
@rm -f $(COQMAKEFILE) $(COQMAKEFILE).conf
1921

2022
uninstall:
21-
$(MAKE) -f Makefile.coq uninstall
22-
23+
$(MAKE) -f $(COQMAKEFILE) uninstall
2324

2425
dist:
2526
@ git archive --prefix coq-ext-lib/ HEAD -o $(PROJECT_NAME).tgz
2627

27-
include tools/Makefile.doc
28+
.PHONY: all clean dist theories examples html
2829

29-
%.md: meta.yml templates/%.md.mustache
30-
mustache $^ > $@
30+
TEMPLATES ?= ../templates
3131

32-
%.html: %.md
33-
pandoc -s -o $@ $<
32+
docs/index.html: index.md
33+
pandoc -s $^ -o $@
3434

35-
.PHONY: all clean dist theories examples html
35+
index.md: meta.yml
36+
$(TEMPLATES)/generate.sh $@

coqdocjs

Lines changed: 0 additions & 1 deletion
This file was deleted.

coqdocjs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
docs/coqdocjs

docs/coqdocjs

Submodule coqdocjs added at 556b3ab

docs/index.html

Lines changed: 56 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,56 @@
1+
<!DOCTYPE html>
2+
<html xmlns="http://www.w3.org/1999/xhtml" lang="en" xml:lang="en">
3+
<head>
4+
<meta charset="utf-8" />
5+
<meta name="generator" content="pandoc" />
6+
<meta name="viewport" content="width=device-width, initial-scale=1.0, user-scalable=yes" />
7+
<title>coq-ext-lib</title>
8+
<style>
9+
code{white-space: pre-wrap;}
10+
span.smallcaps{font-variant: small-caps;}
11+
span.underline{text-decoration: underline;}
12+
div.column{display: inline-block; vertical-align: top; width: 50%;}
13+
div.hanging-indent{margin-left: 1.5em; text-indent: -1.5em;}
14+
ul.task-list{list-style: none;}
15+
</style>
16+
<!--[if lt IE 9]>
17+
<script src="//cdnjs.cloudflare.com/ajax/libs/html5shiv/3.7.3/html5shiv-printshiv.min.js"></script>
18+
<![endif]-->
19+
<style type="text/css"> body {font-family: Arial, Helvetica; margin-left: 5em; font-size: large;} </style>
20+
<style type="text/css"> h1 {margin-left: 0em; padding: 0px; text-align: center} </style>
21+
<style type="text/css"> h2 {margin-left: 0em; padding: 0px; color: #580909} </style>
22+
<style type="text/css"> h3 {margin-left: 1em; padding: 0px; color: #C05001;} </style>
23+
<style type="text/css"> body { width: 1100px; margin-left: 30px; }</style>
24+
</head>
25+
<body>
26+
<header id="title-block-header">
27+
<h1 class="title">coq-ext-lib</h1>
28+
</header>
29+
<div style="text-align:left">
30+
<img src="https://github.githubassets.com/images/modules/logos_page/Octocat.png" height="25" style="border:0px"> <a href="https://github.com/coq-community/coq-ext-lib">View the project on GitHub</a> <img src="https://github.githubassets.com/images/modules/logos_page/Octocat.png" height="25" style="border:0px">
31+
</div>
32+
<h2 id="about">About</h2>
33+
<p>Welcome to the coq-ext-lib project website! This project is part of <a href="https://github.com/coq-community/manifesto">coq-community</a>.</p>
34+
<p>A collection of theories and plugins that may be useful in other Coq developments.</p>
35+
<p>This is an open source project, licensed under the The FreeBSD Copyright.</p>
36+
<h2 id="get-the-code">Get the code</h2>
37+
<p>The current stable release of coq-ext-lib can be <a href="https://github.com/coq-community/coq-ext-lib/releases">downloaded from GitHub</a>.</p>
38+
<h2 id="documentation">Documentation</h2>
39+
<ul>
40+
<li><a href="v0.11.1/toc.html">0.11.1</a></li>
41+
<li><a href="v0.11.0/toc.html">0.11.0</a></li>
42+
<li><a href="v0.10.3/toc.html">0.10.3</a></li>
43+
</ul>
44+
<p>Other related publications, if any, are listed below.</p>
45+
<h2 id="help-and-contact">Help and contact</h2>
46+
<ul>
47+
<li>Report issues on <a href="https://github.com/coq-community/coq-ext-lib/issues">GitHub</a></li>
48+
<li>Chat with us on <a href="https://coq.zulipchat.com/#narrow/stream/237663-coq-community-devs.20.26.20users">Zulip</a></li>
49+
<li>Discuss with us on Coq’s <a href="https://coq.discourse.group">Discourse</a> forum</li>
50+
</ul>
51+
<h2 id="authors-and-contributors">Authors and contributors</h2>
52+
<ul>
53+
<li>Gregory Malecha</li>
54+
</ul>
55+
</body>
56+
</html>

docs/v0.10.3/ExtLib.Core.Any.html

Lines changed: 62 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,62 @@
1+
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
2+
<html xmlns="http://www.w3.org/1999/xhtml">
3+
4+
<head>
5+
<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
6+
<link href="resources/coqdoc.css" rel="stylesheet" type="text/css" />
7+
<link href="resources/coqdocjs.css" rel="stylesheet" type="text/css"/>
8+
<script type="text/javascript" src="resources/config.js"></script>
9+
<script type="text/javascript" src="resources/coqdocjs.js"></script>
10+
</head>
11+
12+
<body onload="document.getElementById('content').focus()">
13+
<div id="header">
14+
<span class="left">
15+
<span class="modulename"> <script> document.write(document.title) </script> </span>
16+
</span>
17+
18+
<span class="button" id="toggle-proofs"></span>
19+
20+
<span class="right">
21+
<a href="../">Project Page</a>
22+
<a href="./indexpage.html"> Index </a>
23+
<a href="./toc.html"> Table of Contents </a>
24+
</span>
25+
</div>
26+
<div id="content" tabindex="-1" onblur="document.getElementById('content').focus()">
27+
<div id="main">
28+
<h1 class="libtitle">ExtLib.Core.Any</h1>
29+
30+
<div class="code">
31+
<span class="id" title="keyword">Set Implicit Arguments</span>.<br/>
32+
<span class="id" title="keyword">Set</span> <span class="id" title="keyword">Strict</span> <span class="id" title="keyword">Implicit</span>.<br/>
33+
34+
<br/>
35+
</div>
36+
37+
<div class="doc">
38+
This class should be used when no requirements are needed
39+
</div>
40+
<div class="code">
41+
<span class="id" title="var">Polymorphic</span> <span class="id" title="keyword">Class</span> <a name="Any"><span class="id" title="record">Any</span></a> (<span class="id" title="var">T</span> : <span class="id" title="keyword">Type</span>) : <span class="id" title="keyword">Type</span>.<br/>
42+
43+
<br/>
44+
<span class="id" title="keyword">Global</span> <span class="id" title="var">Polymorphic</span> <span class="id" title="keyword">Instance</span> <a name="Any_a"><span class="id" title="instance">Any_a</span></a> (<span class="id" title="var">T</span> : <span class="id" title="keyword">Type</span>) : <a class="idref" href="ExtLib.Core.Any.html#Any"><span class="id" title="class">Any</span></a> <a class="idref" href="ExtLib.Core.Any.html#T"><span class="id" title="variable">T</span></a> := {}.<br/>
45+
46+
<br/>
47+
<span class="id" title="var">Polymorphic</span> <span class="id" title="keyword">Definition</span> <a name="RESOLVE"><span class="id" title="definition">RESOLVE</span></a> (<span class="id" title="var">T</span> : <span class="id" title="keyword">Type</span>) : <span class="id" title="keyword">Type</span> := <a class="idref" href="ExtLib.Core.Any.html#T"><span class="id" title="variable">T</span></a>.<br/>
48+
49+
<br/>
50+
<span class="id" title="var">Existing</span> <span class="id" title="keyword">Class</span> <span class="id" title="var">RESOLVE</span>.<br/>
51+
52+
<br/>
53+
<span class="id" title="keyword">Hint Extern</span> 0 (<a class="idref" href="ExtLib.Core.Any.html#RESOLVE"><span class="id" title="class">RESOLVE</span></a> <span class="id" title="var">_</span>) =&gt; <span class="id" title="tactic">unfold</span> <a class="idref" href="ExtLib.Core.Any.html#RESOLVE"><span class="id" title="class">RESOLVE</span></a> : <span class="id" title="var">typeclass_instances</span>.<br/>
54+
</div>
55+
</div>
56+
<div id="footer">
57+
Generated by <a href="http://coq.inria.fr/">coqdoc</a> and improved with <a href="https://github.com/tebbi/coqdocjs">CoqdocJS</a>
58+
</div>
59+
</div>
60+
</body>
61+
62+
</html>

0 commit comments

Comments
 (0)