-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathREADME.devel
81 lines (54 loc) · 2.59 KB
/
README.devel
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
SimSoC-Cert, a toolkit for generating certified processor simulators
See the COPYRIGHTS and LICENSE files
--------------------------------------------------------------------
Guideline for SimSoC-Cert 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.
About compilation:
------------------
- Before any commit, make sure that it compiles with the last stable
release of Coq and, if possible, with the development version of
Coq.
- Put useful messages when you commit.
- When you add a file, do "make config" to build Makefile.Coq and the
dependencies again.
About the coding style:
-----------------------
- Try to follow the style currently used.
- Use maximum 78 characters per line.
- Add the SimSoC-Cert 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.
- Define decidability lemmas using boolean function.
- Avoid decidability lemmas. Use boolean functions instead.
- Try to define equivalence lemmas whenever possible in order to use
rewriting.
- 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,
(*WARNING:...*) for adding some important remark
(e.g. something can could be improved),
(*REMOVE:...*) for indicating something to be removed,
(*MOVE:...*) for indicating something to be moved,
(*IMPROVE:...*) for indicating soemthing that could be improved.