Skip to content

Commit d86043c

Browse files
yurrriqyurrriq
committed
CONTRIBUTING.md: start fleshing out content
1 parent 5c7e9e8 commit d86043c

File tree

2 files changed

+266
-1
lines changed

2 files changed

+266
-1
lines changed

‎CONTRIBUTING.md

Lines changed: 148 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,150 @@
11
## Contributing
22

3-
_TBD_ (see [issue #4](https://github.com/idris-hackers/software-foundations/issues/4) for discussion)
3+
_TBD_ (see [issue #4] for discussion)
4+
5+
### General Workflow
6+
7+
_TODO: write me_
8+
9+
10+
### Formatting
11+
12+
When formatting the [Literate Idris] source, we use [bird tracks] for code meant
13+
to be compiled and a combination of [Markdown] and [LaTeX] for commentary and
14+
illustrative examples that aren't meant to be compiled.
15+
16+
````markdown
17+
= Example
18+
19+
This is some commentary with **bold** and _italicized_ text.
20+
21+
```idris
22+
-- This is an Idris code block which won't be read when compiling the file.
23+
foo : Nat
24+
foo = 42
25+
```
26+
27+
28+
== Code to Compile
29+
30+
The following, however, will be compiled:
31+
32+
> module Example
33+
>
34+
> %access public export
35+
>
36+
> foo : String
37+
> foo = "bar"
38+
39+
40+
== Other Notes
41+
42+
- We can also highlight code inline, e.g. \idr{primes : Inf (List Nat)}.
43+
- To refer to glossary entries, use e.g. \mintinline[]{latex}{\gls{term}}.
44+
````
45+
46+
#### Chapters, Sections, et al.
47+
48+
To denote chapters, sections, and other subdivisions, use `=` as follows:
49+
50+
```markdown
51+
= Chapter
52+
== Section
53+
=== Subsection
54+
==== Subsubsection
55+
```
56+
57+
#### Bold and Italicized Text
58+
59+
We use the succinct Markdown syntax...
60+
61+
```markdown
62+
... to format **bold** and _italicized_ text.
63+
```
64+
65+
#### Lists
66+
67+
We prefer the Markdown syntax here too, e.g.
68+
69+
```markdown
70+
- foo
71+
- bar
72+
- baz
73+
```
74+
75+
#### Code Blocks
76+
77+
Just as with bold and italicized text, we favor the more succinct Markdown
78+
syntax for (fenced) code blocks:
79+
80+
````markdown
81+
```idris
82+
addTwo : Nat -> Nat
83+
addTwo x = x + 2
84+
```
85+
````
86+
87+
For more information, refer to [the relevant GitHub Help document][gfm code blocks].
88+
89+
#### Inline Code
90+
91+
For inline Idris code, use the custom `\mintinline` shortcut `\idr`, e.g.
92+
93+
```tex
94+
To print ``Hello World!'' in Idris, write \idr{putStrLn "Hello, World!"}.
95+
```
96+
97+
For convenience, we've also defined the shortcut `\el` for ineline Emacs Lisp
98+
code, e.g.
99+
100+
```latex
101+
Set the value of \el{foo} to \el{42}: \el{(setq foo 42)}.
102+
```
103+
104+
Otherwise, use single backticks for inline monospace text, e.g.
105+
106+
```
107+
This is some `inline monospaced text`.
108+
```
109+
110+
In a certain cases, we might want syntax highlighting for a language other than
111+
Idris or Emacs Lisp. For such cases, use the standard `\mintline` command, e.g.
112+
113+
```tex
114+
To declare a theorem in Coq, use \mintinline[]{coq}{Theorem}.
115+
```
116+
117+
#### Glossary
118+
119+
We use the [glossaries package] for defining terms
120+
(in [`src/glossary.tex`][glossary.tex]) and including a glossary in
121+
the [generated PDF][PDF]. See the package documentation for more information,
122+
but here's a quick example:
123+
124+
```tex
125+
What is the \gls{meaning of life}?
126+
127+
128+
\newglossaryentry{meaning of life}{
129+
description={42}
130+
}
131+
```
132+
133+
134+
### Generating the PDF
135+
136+
To generate the [PDF] we use [Pandoc] and [latexmk]. For more details, check out
137+
the `all.pdf`, `all.tex` and `%.tex` rules in [`src/Makefile`].
138+
139+
140+
<!-- Named Links -->
141+
142+
[issue #4]: https://github.com/idris-hackers/software-foundations/issues/4
143+
[Literate Idris]: http://docs.idris-lang.org/en/latest/tutorial/miscellany.html#literate-programming
144+
[bird tracks]: https://wiki.haskell.org/Literate_programming#Bird_Style
145+
[Markdown]: https://daringfireball.net/projects/markdown/
146+
[LaTeX]: http://www.latex-project.org
147+
[gfm code blocks]: https://help.github.com/articles/creating-and-highlighting-code-blocks/
148+
[glossaries package]: https://www.ctan.org/pkg/glossaries
149+
[glossary.tex]: https://github.com/idris-hackers/software-foundations/blob/master/src/glossary.tex
150+
[`src/Makefile`]: https://github.com/idris-hackers/software-foundations/blob/master/src/glossary.tex

‎docs/index.html

Lines changed: 118 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,43 @@
66
<meta name="generator" content="pandoc" />
77
<title></title>
88
<style type="text/css">code{white-space: pre;}</style>
9+
<style type="text/css">
10+
div.sourceCode { overflow-x: auto; }
11+
table.sourceCode, tr.sourceCode, td.lineNumbers, td.sourceCode {
12+
margin: 0; padding: 0; vertical-align: baseline; border: none; }
13+
table.sourceCode { width: 100%; line-height: 100%; }
14+
td.lineNumbers { text-align: right; padding-right: 4px; padding-left: 4px; color: #aaaaaa; border-right: 1px solid #aaaaaa; }
15+
td.sourceCode { padding-left: 5px; }
16+
code > span.kw { color: #007020; font-weight: bold; } /* Keyword */
17+
code > span.dt { color: #902000; } /* DataType */
18+
code > span.dv { color: #40a070; } /* DecVal */
19+
code > span.bn { color: #40a070; } /* BaseN */
20+
code > span.fl { color: #40a070; } /* Float */
21+
code > span.ch { color: #4070a0; } /* Char */
22+
code > span.st { color: #4070a0; } /* String */
23+
code > span.co { color: #60a0b0; font-style: italic; } /* Comment */
24+
code > span.ot { color: #007020; } /* Other */
25+
code > span.al { color: #ff0000; font-weight: bold; } /* Alert */
26+
code > span.fu { color: #06287e; } /* Function */
27+
code > span.er { color: #ff0000; font-weight: bold; } /* Error */
28+
code > span.wa { color: #60a0b0; font-weight: bold; font-style: italic; } /* Warning */
29+
code > span.cn { color: #880000; } /* Constant */
30+
code > span.sc { color: #4070a0; } /* SpecialChar */
31+
code > span.vs { color: #4070a0; } /* VerbatimString */
32+
code > span.ss { color: #bb6688; } /* SpecialString */
33+
code > span.im { } /* Import */
34+
code > span.va { color: #19177c; } /* Variable */
35+
code > span.cf { color: #007020; font-weight: bold; } /* ControlFlow */
36+
code > span.op { color: #666666; } /* Operator */
37+
code > span.bu { } /* BuiltIn */
38+
code > span.ex { } /* Extension */
39+
code > span.pp { color: #bc7a00; } /* Preprocessor */
40+
code > span.at { color: #7d9029; } /* Attribute */
41+
code > span.do { color: #ba2121; font-style: italic; } /* Documentation */
42+
code > span.an { color: #60a0b0; font-weight: bold; font-style: italic; } /* Annotation */
43+
code > span.cv { color: #60a0b0; font-weight: bold; font-style: italic; } /* CommentVar */
44+
code > span.in { color: #60a0b0; font-weight: bold; font-style: italic; } /* Information */
45+
</style>
946
</head>
1047
<body>
1148
<h1 id="software-foundations-in-idris"><em><a href="http://www.cis.upenn.edu/%7Ebcpierce/sf/current/index.html">Software Foundations</a> in Idris</em></h1>
@@ -72,5 +109,86 @@ <h3 id="prerequisites">Prerequisites</h3>
72109
<!-- Named Links -->
73110
<h2 id="contributing">Contributing</h2>
74111
<p><em>TBD</em> (see <a href="https://github.com/idris-hackers/software-foundations/issues/4">issue #4</a> for discussion)</p>
112+
<h3 id="general-workflow">General Workflow</h3>
113+
<p><em>TODO: write me</em></p>
114+
<h3 id="formatting">Formatting</h3>
115+
<p>When formatting the <a href="http://docs.idris-lang.org/en/latest/tutorial/miscellany.html#literate-programming">Literate Idris</a> source, we use <a href="https://wiki.haskell.org/Literate_programming#Bird_Style">bird tracks</a> for code meant<br />
116+
to be compiled and a combination of <a href="https://daringfireball.net/projects/markdown/">Markdown</a> and <a href="http://www.latex-project.org">LaTeX</a> for commentary and<br />
117+
illustrative examples that aren't meant to be compiled.</p>
118+
<div class="sourceCode"><pre class="sourceCode markdown"><code class="sourceCode markdown">= Example
119+
120+
This is some commentary with **bold** and _italicized_ text.
121+
122+
```idris
123+
-- This is an Idris code block which won&#39;t be read when compiling the file.
124+
foo : Nat
125+
foo = 42
126+
```
127+
128+
129+
== Code to Compile
130+
131+
The following, however, will be compiled:
132+
133+
&gt;<span class="dt"> module Example</span>
134+
<span class="dt">&gt;</span>
135+
<span class="dt">&gt; %access public export</span>
136+
<span class="dt">&gt;</span>
137+
<span class="dt">&gt; foo : String</span>
138+
<span class="dt">&gt; foo = &quot;bar&quot;</span>
139+
140+
141+
== Other Notes
142+
143+
- <span class="fl">We can also highlight code inline, e.g. \idr{primes : Inf (List Nat)}.</span>
144+
<span class="fl">- To refer to glossary entries, use e.g. \mintinline[]{latex}{\gls{term}}.</span></code></pre></div>
145+
<h4 id="chapters-sections-et-al.">Chapters, Sections, et al.</h4>
146+
<p>To denote chapters, sections, and other subdivisions, use <code>=</code> as follows:</p>
147+
<div class="sourceCode"><pre class="sourceCode markdown"><code class="sourceCode markdown">= Chapter
148+
== Section
149+
=== Subsection
150+
==== Subsubsection</code></pre></div>
151+
<h4 id="bold-and-italicized-text">Bold and Italicized Text</h4>
152+
<p>We use the succinct Markdown syntax...</p>
153+
<div class="sourceCode"><pre class="sourceCode markdown"><code class="sourceCode markdown">... to format **bold** and _italicized_ text.</code></pre></div>
154+
<h4 id="lists">Lists</h4>
155+
<p>We prefer the Markdown syntax here too, e.g.</p>
156+
<div class="sourceCode"><pre class="sourceCode markdown"><code class="sourceCode markdown">- <span class="fl">foo</span>
157+
<span class="fl">- bar</span>
158+
<span class="fl">- baz</span></code></pre></div>
159+
<h4 id="code-blocks">Code Blocks</h4>
160+
<p>Just as with bold and italicized text, we favor the more succinct Markdown<br />
161+
syntax for (fenced) code blocks:</p>
162+
<div class="sourceCode"><pre class="sourceCode markdown"><code class="sourceCode markdown">```idris
163+
addTwo : Nat -&gt; Nat
164+
addTwo x = x + 2
165+
```</code></pre></div>
166+
<p>For more information, refer to <a href="https://help.github.com/articles/creating-and-highlighting-code-blocks/">the relevant GitHub Help document</a>.</p>
167+
<h4 id="inline-code">Inline Code</h4>
168+
<p>For inline Idris code, use the custom <code>\mintinline</code> shortcut <code>\idr</code>, e.g.</p>
169+
<div class="sourceCode"><pre class="sourceCode tex"><code class="sourceCode latex">To print ``Hello World!&#39;&#39; in Idris, write <span class="fu">\idr</span>{putStrLn &quot;Hello, World!&quot;}.</code></pre></div>
170+
<p>For convenience, we've also defined the shortcut <code>\el</code> for ineline Emacs Lisp<br />
171+
code, e.g.</p>
172+
<div class="sourceCode"><pre class="sourceCode latex"><code class="sourceCode latex">Set the value of <span class="fu">\el</span>{foo} to <span class="fu">\el</span>{42}: <span class="fu">\el</span>{(setq foo 42)}.</code></pre></div>
173+
<p>Otherwise, use single backticks for inline monospace text, e.g.</p>
174+
<pre><code>This is some `inline monospaced text`.</code></pre>
175+
<p>In a certain cases, we might want syntax highlighting for a language other than<br />
176+
Idris or Emacs Lisp. For such cases, use the standard <code>\mintline</code> command, e.g.</p>
177+
<div class="sourceCode"><pre class="sourceCode tex"><code class="sourceCode latex">To declare a theorem in Coq, use <span class="fu">\mintinline</span>[]{coq}{Theorem}.</code></pre></div>
178+
<h4 id="glossary">Glossary</h4>
179+
<p>We use the <a href="https://www.ctan.org/pkg/glossaries">glossaries package</a> for defining terms<br />
180+
(in <a href="https://github.com/idris-hackers/software-foundations/blob/master/src/glossary.tex"><code>src/glossary.tex</code></a>) and including a glossary in<br />
181+
the [generated PDF][PDF]. See the package documentation for more information,<br />
182+
but here's a quick example:</p>
183+
<div class="sourceCode"><pre class="sourceCode tex"><code class="sourceCode latex">What is the <span class="fu">\gls</span>{meaning of life}?
184+
185+
186+
<span class="fu">\newglossaryentry</span>{meaning of life}{
187+
description={42}
188+
}</code></pre></div>
189+
<h3 id="generating-the-pdf">Generating the PDF</h3>
190+
<p>To generate the [PDF] we use [Pandoc] and [latexmk]. For more details, check out<br />
191+
the <code>all.pdf</code>, <code>all.tex</code> and <code>%.tex</code> rules in <a href="https://github.com/idris-hackers/software-foundations/blob/master/src/glossary.tex"><code>src/Makefile</code></a>.</p>
192+
<!-- Named Links -->
75193
</body>
76194
</html>

0 commit comments

Comments
 (0)