-
Notifications
You must be signed in to change notification settings - Fork 46
/
meta.yml
111 lines (99 loc) · 3.53 KB
/
meta.yml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
---
fullname: coq-ext-lib
shortname: coq-ext-lib
opam_name: coq-ext-lib
organization: coq-community
community: true
action: true
ci_test_dependants: true
submodule: true
synopsis: A library of Coq definitions, theorems, and tactics
description: A collection of theories and plugins that may be useful in other Coq developments.
authors:
- name: Gregory Malecha
initial: true
maintainers:
- name: Gregory Malecha
nickname: gmalecha
- name: Yishuai Li
nickname: liyishuai
opam-file-maintainer: "gmalecha@gmail.com"
license:
fullname: BSD 2-Clause "Simplified" License
identifier: BSD-2-Clause
supported_coq_versions:
text: Coq 8.11 or later or 8.9
opam: '{ >= "8.9" < "8.10" | >= "8.11" }'
tested_coq_opam_versions:
- version: '8.9'
- version: '8.11'
- version: '8.12'
- version: '8.13'
- version: '8.14'
- version: '8.15'
- version: '8.16'
- version: '8.17'
- version: '8.18'
- version: '8.19'
- version: 'dev'
make_target: theories
test_target: examples
namespace: ExtLib
action_appendix: |2-
set -o pipefail # recommended if the script uses pipes
startGroup "Generate Coqdoc"
make -j`nproc` coqdoc
endGroup
before_script: |
startGroup "Workaround permission issue"
sudo chown -R coq:coq .
endGroup
export: 'OPAMWITHTEST OPAMCONFIRMLEVEL'
env:
OPAMWITHTEST: true
OPAMCONFIRMLEVEL: unsafe-yes
- name: Revert permissions
# to avoid a warning at cleanup time
if: ${{ always() }}
run: sudo chown -R 1001:116 .
- uses: actions/upload-artifact@v4
with:
name: coqdoc
path: html
overwrite: true
documentation: |
Ideas
-----
- Embrace new features, e.g. universe polymorphism, primitive projections, etc.
- Use modules for controlling namespaces.
- Use first-class abstractions where appropriate, e.g. type classes, canonical structures, etc.
- The library is mostly built around type clases
- Notations should be hidden by modules that are explicitly opened.
- This avoids clashes between precedence.
- TB: Actually, this does not completely avoid clashes, if we have to open two modules at the same time (for instance, I often need to open Equality, to get dependent destruction, which conflicts with the rest of my development)
- TB: I like the idea of having to prefix operations by the name of the module (e.g., DList.fold, DList.map, DList.T), and yet to benefit from the support of notations, without opening this module. I implement that by having a module DList that contains the operations, inside the file DList. The notations live in the file DList, and I do Require Import DList everywhere...
- Avoid the use of the 'core' hint database.
- Avoid the use of dependent functions, e.g. dependendent decidable equality,
in favor of their boolen counter-parts. Use type-classes to expose the proofs.
-
File Structure
--------------
* theories/
- Base directory to the provided theories
coqdoc: true
index_documentation: |
Documentation
-------------
- [0.12.1](v0.12.1/toc.html)
- [0.12.0](v0.12.0/toc.html)
- [0.11.8](v0.11.8/toc.html)
- [0.11.7](v0.11.7/toc.html)
- [0.11.6](v0.11.6/toc.html) (final support for Coq 8.8 and 8.10)
- [0.11.5](v0.11.5/toc.html)
- [0.11.4](v0.11.4/toc.html)
- [0.11.3](v0.11.3/toc.html)
- [0.11.2](v0.11.2/toc.html)
- [0.11.1](v0.11.1/toc.html)
- [0.11.0](v0.11.0/toc.html)
- [0.10.3](v0.10.3/toc.html)
---