-
Notifications
You must be signed in to change notification settings - Fork 21
/
Copy pathCONTRIBUTING
117 lines (84 loc) · 3.68 KB
/
CONTRIBUTING
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
112
113
114
115
116
117
Guideline for CoLoR developers
------------------------------
- For new contributors, update the COPYRIGHT file.
- Don't forget to update the CHANGES and THANKS files.
- If you bring important modifications to an already existing file,
add in the header your name with the modification date yy-mm-dd.
How to create a new release:
----------------------------
In ~/color-svn:
- check that every compiles: make clean-all && make && make doc
- update CHANGES, README and INSTALL
- make install-doc
- make install-dist
- commit your changes
- ./create_dist $new_version_name (e.g. 1.4.0)
(it computes md5sum color.$new_version_name)
- check that color.$new_version_name compiles
- add color.$new_version_name on https://gforge.inria.fr/frs/?group_id=467
In ~/src/opam-coq-archive-fblanqui-git:
- update-from-remote
- cd released/packages/coq-color
- cp coq-color.$old_version_name coq-color.$new_version_name
- cd coq-color.$new_version_name
- update descr, opam and url
- nettoie
- cd ..
- add coq-color.$new_version_name
- ci -m "$comment"
On https://github.com/fblanqui/opam-coq-archive:
- create a pull request
In ~/rewriting-svn/web:
- update color/index.html
- make
- make install
After pull request approval, send a mail to color@inria.fr.
About compilation:
------------------
- Before any commit, make sure that CoLoR compiles with the last
stable release of Coq and, if possible, with the development version
of Coq. Check also that Rainbow examples still work.
- Put useful messages when you commit.
- When you add a file, do "make config" to build Makefile.Coq and the
dependencies again.
About the CoLoR style:
----------------------
- Try to follow the style currently used in CoLoR.
- Use maximum 78 characters per line.
- Add the CoLoR header at the beginning of each file with the creation
date yy-mm-dd.
- Only use Parameter, Definition, Lemma (no Axiom, Theorem, etc.).
- Put comments! And use the possibilities offered by coqdoc. For
instance, "(** " creates a section title. Check the result by doing
"make doc".
- Try to use the Coq standard library as much as possible except for
the definition of well-foundedness: it is redefined in
Util/Relation/SN.v.
- Definitions and lemmas about structures of general interest must be
put in Util. Term structures are in Term and every termination
technique must be put in a new directory at the root of the project.
- Files about algebraic terms (Term/WithArity) should be prefixed with
A. Files about varyadic terms (Term/Varyadic) should be prefixed with
V.
- Define decidability lemmas using boolean function.
- Do not use setoid rewrites in decidability lemmas.
- Try to build the names of lemmas by concatening its main
ingredients. For instance:
Lemma Vforall_in : forall P x n (v : vec n), Vforall P v -> Vin x v -> P x.
You can also add the suffix "intro" or "elim" for specifying its
use. For instance:
Lemma Vforall_intro : forall (P : A->Prop) n (v : vec n),
(forall x, Vin x v -> P x) -> Vforall P v.
provides a way of proving Vforall (introduction rule).
Lemma Vin_elim : forall x n (v : vec n),
Vin x v -> exists n1, exists v1 : vec n1, exists n2, exists v2 : vec n2,
exists H : n1 + S n2 = n, v = Vcast (Vapp v1 (Vcons x v2)) H.
provides a way to deduce some information from Vin (elimination rule).
- Use "Require Export" as less as possible. Use "Require Import"
instead. This reduces the compilation time.
- Use (*COQ:...*) for indicating problems with Coq,
(*FIXME:...*) for indicating something to be fixed,
(*REMARK:...*) for adding some important remark
(e.g. something that could be improved),
(*REMOVE:...*) for indicating something to be removed,
(*MOVE:...*) for indicating something to be moved.