| Age | Commit message (Collapse) | Author |
|---|
|
Otherwise they will be typeset as if the end of a sentence, causing
additional spacing after the '.' when not using \frenchspacing.
|
|
Add more latex tests and fix underscore escaping
|
|
|
|
|
|
|
|
This refactoring is intended to allow this type to have more than just a
list of definitions in future.
|
|
Handle sectioning commands in saildoc LaTeX output
|
|
|
|
|
|
This ensures names shared between multiple projects don't collide if
included in a common LaTeX document; cheri-architecture using both
sail-cheri-mips and sail-cheri-riscv runs into this.
Closes: #88
|
|
Now that the category is prepended in latex_cat_id, also prepend
opt_prefix there instead to ensure no caller forgets to do so.
No functional change intended, and verified by regenerating the LaTeX
for sail-cheri-mips and sail-cheri-riscv.
|
|
Rather than having the caller prefix latex and refcode strings with the
category, push that down into common functions to both abstract away the
details and avoid duplication.
No functional change intended, and verified by regenerating the LaTeX
for sail-cheri-mips and sail-cheri-riscv.
|
|
|
|
This can be useful to reference things that aren't defined by sail.
|
|
This takes two arguments: the label name and the \saildocfoo macro use
itself. This allows cunning definitions of \saildoclabelled and
\saildocfoo to tease apart the various bits and reconstruct them in a
different order without having to redefine \phantomsection and \label
temporarily and hard-code knowledge of the implementation of these
documentation commands. I intend to use these in cheri-architecture in
combination with sail-cheri-riscv.
Unlike the other macros, this is considered a bit more niche, so we
include a default definition of it that expands to what was previously
hard-coded. This also makes this a non-breaking change.
|
|
|
|
Printing the text is only so helpful; the most important thing to know
is what kind of element it actually is, which is lost when extracting
the text. Instead, print the whole S-Expr.
|
|
Also add a $suppress_warnings directive that ensures that no warnings
are generated for a specific file.
|
|
Add a new short_loc_to_string function that produces just the file and line number as
a single line. loc_to_string adds a bunch of terminal color codes and other formatting
designed for producing pretty error-messages in the terminal, which isn't ideal when
the string appears in prover output as part of an assert statement. This is should be
purely an aesthetic change.
|
|
Fixes #33
|
|
|
|
since riscv is no longer in this repository, and we use the RISC-V
duopod as an example, you need to build as:
make RISCV=directory manual.pdf
if directory is not equal to ../../sail-riscv (which is where it would
be if sail and sail-riscv are checked out in the same respository
together)
|
|
|
|
details (TODO make this optional).
|
|
|
|
usere more flexibility about formatting generated latex.
|
|
|
|
Also ensure no collisions for function clause constructor categories
|
|
|
|
The main changes so far are:
* Allow markdown formatting in doc comments. We parse the markdown
using Omd, which is a OCaml library for parsing markdown. The nice
thing about this library is it's pure OCaml and has no dependencies
other the the stdlib. Incidentally it was also developed at OCaml
labs. Using markdown keeps our doc-comments from becoming latex
specfic, and having an actual parser is _much_ nicer than trying to
hackily process latex in doc-comments using OCamls somewhat sub-par
regex support.
* More sane conversion latex identifiers the main approach is to
convert Sail identifiers to lowerCamelCase, replacing numbers with
words, and then add a 'category' code based on the type of
identifier, so for a function we'd have fnlowerCamelCase and for
type synonym typelowerCamelCase etc. Because this transformation is
non-injective we keep track of identifiers we've generated so we end
up with identifierA, identifierB, identifierC when there are
collisions.
* Because we parse markdown in doc comments doc comments can use Sail
identifiers directly in hyperlinks, without having to care about how
they are name-mangled down into TeX compatible things.
* Allow directives to be passed through the compiler to
backends. There are various $latex directives that modify the latex
output. Most usefully there's a
$latex newcommand name markdown
directive that uses the markdown parser to generate latex
commands. An example of why this is useful is bellow. We can also use
$latex noref id
To suppress automatically inserting links to an identifier
* Refactor the latex generator to make the overall generation process
cleaner
* Work around the fact that some operating systems consider
case-sensitive file names to be a good thing
* Fix a bug where latex generation wouldn't occur unless the directory
specified by -o didn't exist
This isn't quite all the requested features for good CHERI
documentation, but new features should be much easier to add now.
|
|
There is no Reporting_complex, so it's not clear what the basic is
intended to signify anyway.
Add a GitHub issue link to any err_unreachable errors (as they are all
bugs)
|
|
Now that Jenkins is updated to a newer version of OCaml we can finally
fix some warning with more recent versions of OCaml than 4.02.3. Also
fix a Lem test case that was failing.
|
|
One day we will be free from the 4.02.3 menace, but today is not that day. :(
This should fix Sail on Jenkins
This reverts commit 86e29bcbb1597c4ef1f6cae8edbeed42f9a31414.
|
|
Changes are:
- String.capitalize -> String.capitalize_ascii
- String.uppercase -> String.uppercase_ascii
- String.lowercase -> String.lowercase_ascii
Basically just making the change that the warning message suggested.
|
|
|
|
confusion on case insensitive file systems (e.g. mac).
|
|
of omitting valspec in documentation if it is deemed too verbose and still have hyperlinks work. The caveat is that it could result in multiply defined labels.
|
|
with documents containing listings in multiple languages.
|
|
|
|
|
|
|
|
|
|
More work on Latex output
|
|
Now generate commands for each toplevel definition, such that e.g. the
function clause for execute LOAD could be inserted using
\sailexecuteLOAD. Tries to generate fairly intuitive names while
avoiding clashes where possible.
|
|
Can now compile RISCV. Requires some library tweaks before it'll pass any tests,
Also adds hyperlinks to wip latex output
|
|
Added option -latex that outputs input to a latex document.
Added doc comments that can be attached to certain AST nodes - right now just valspecs and function clauses, e.g.
/*!
Documentation for main
*/
val main : unit -> unit
These comments are kept by the sail pretty printer, and used when generating latex
|
