| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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
|
