You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
<p><em>TBD</em> (see <ahref="https://github.com/idris-hackers/software-foundations/issues/4">issue #4</a> for discussion)</p>
112
112
<h3id="general-workflow">General Workflow</h3>
113
-
<p><em>TODO: write me</em></p>
113
+
<ol>
114
+
<li><ahref="https://github.com/idris-hackers/software-foundations/fork">Fork the repository</a> if you haven't already.</li>
115
+
<li>Check the <ahref="https://github.com/idris-hackers/software-foundations/pulls">open pull requests</a> for any related work in progress (WIP).</li>
116
+
<li>Check out a new branch based on <code>develop</code>.</li>
117
+
<li>Push some commits to your fork.</li>
118
+
</ol>
119
+
<ul>
120
+
<li>The general workflow here is as follows:
121
+
<ul>
122
+
<li>Copy/paste the original text, <ahref="#formatting">reformatting</a> as<br/>
123
+
appropriate.</li>
124
+
<li>Translate Coq code into (idiomatic) Idris.</li>
125
+
<li>Edit, augment and delete text as appropriate.<br/>
126
+
<em>N.B. This can be done in subsequent pull requests.</em></li>
127
+
</ul></li>
128
+
</ul>
129
+
<ol>
130
+
<li>Open a pull request (as soon as possible).</li>
131
+
</ol>
132
+
<ul>
133
+
<li>If it's not ready to be merged, but you want to <em>claim</em> a particular task,<br/>
134
+
prefix the pull request with <code>WIP:</code>.</li>
135
+
<li>Make a comment and remove the <code>WIP:</code> when it's ready to be reviewed and<br/>
136
+
merged. <em>Remember: formatting the text and taking a first pass at<br/>
137
+
translating the Coq to Idris is enough for an initial pull request.</em></li>
138
+
</ul>
139
+
<ol>
140
+
<li>Open subsequent pull requests following a similar pattern for and edits or<br/>
141
+
other updates</li>
142
+
</ol>
143
+
<p>The <code>develop</code> branch is the <em>working branch</em> and <code>master</code> is for <em>releases</em>,<br/>
144
+
i.e. rebuilt <ahref="https://idris-hackers.github.io/software-foundations/pdf/sf-idris-2016.pdf">PDF</a>s and <ahref="https://idris-hackers.github.io/software-foundations">website</a> updates.</p>
114
145
<h3id="formatting">Formatting</h3>
115
146
<p>When formatting the <ahref="http://docs.idris-lang.org/en/latest/tutorial/miscellany.html#literate-programming">Literate Idris</a> source, we use <ahref="https://wiki.haskell.org/Literate_programming#Bird_Style">bird tracks</a> for code meant<br/>
116
147
to be compiled and a combination of <ahref="https://daringfireball.net/projects/markdown/">Markdown</a> and <ahref="http://www.latex-project.org">LaTeX</a> for commentary and<br/>
<p>For convenience, we've also defined the shortcut <code>\el</code> for ineline Emacs Lisp<br/>
201
+
<p>For convenience, we've also defined the shortcut <code>\el</code> for inline Emacs Lisp<br/>
171
202
code, e.g.</p>
172
203
<divclass="sourceCode"><preclass="sourceCode latex"><codeclass="sourceCode latex">Set the value of <spanclass="fu">\el</span>{foo} to <spanclass="fu">\el</span>{42}: <spanclass="fu">\el</span>{(setq foo 42)}.</code></pre></div>
173
204
<p>Otherwise, use single backticks for inline monospace text, e.g.</p>
174
205
<pre><code>This is some `inline monospaced text`.</code></pre>
175
206
<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>
207
+
Idris or Emacs Lisp. For such cases, use the standard <code>\mintinline</code> command,<br/>
208
+
e.g.</p>
177
209
<divclass="sourceCode"><preclass="sourceCode tex"><codeclass="sourceCode latex">To declare a theorem in Coq, use <spanclass="fu">\mintinline</span>[]{coq}{Theorem}.</code></pre></div>
178
210
<h4id="glossary">Glossary</h4>
179
211
<p>We use the <ahref="https://www.ctan.org/pkg/glossaries">glossaries package</a> for defining terms<br/>
180
212
(in <ahref="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/>
213
+
the <ahref="https://idris-hackers.github.io/software-foundations/pdf/sf-idris-2016.pdf">generated PDF</a>. See the package documentation for more information,<br/>
182
214
but here's a quick example:</p>
183
215
<divclass="sourceCode"><preclass="sourceCode tex"><codeclass="sourceCode latex">What is the <spanclass="fu">\gls</span>{meaning of life}?
<h3id="generating-the-pdf">Generating the PDF</h3>
190
-
<p>To generate the [PDF] we use [Pandoc] and [latexmk]. For more details, check out<br/>
222
+
<p>To generate the <ahref="https://idris-hackers.github.io/software-foundations/pdf/sf-idris-2016.pdf">PDF</a> we use <ahref="http://pandoc.org">Pandoc</a> and <ahref="https://www.ctan.org/pkg/latexmk/">latexmk</a>. For more details, check out<br/>
191
223
the <code>all.pdf</code>, <code>all.tex</code> and <code>%.tex</code> rules in <ahref="https://github.com/idris-hackers/software-foundations/blob/master/src/glossary.tex"><code>src/Makefile</code></a>.</p>
0 commit comments