| Age | Commit message (Collapse) | Author |
|---|
|
Add more latex tests and fix underscore escaping
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Change internal terminology so we more clearly distinguish between a list of
definitions 'defs' and functions that take an entire abstract syntax
trees 'ast'.
|
|
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
|
|
latex: Prefix label names with the specified -latex_prefix
|
|
|
|
|
|
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.
|
|
|
|
Add latex tests and allow external links
|
|
Wrap saildoc LaTeX in \saildoclabelled macro
|
|
This can be useful to reference things that aren't defined by sail.
|
|
This is for a bug I encountered while moving some docs over from the ISA
spec into sail documentation comments.
|
|
Also fix a few shellcheck warnings related to printf while doing so.
|
|
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.
|
|
Saildoc improvements
|
|
C codegen: remove an unnecessary declaration in the header file
|
|
|
|
This seems to be the current name for the overload.
|
|
|
|
|
|
|
|
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.
|
|
We now parse
/*!
* Paragraph
*/
and
/*!
*Paragraph
*/
the same as
/*!
Paragraph
*/
since the first form is prettier, and similar to what Doxygen, Javadoc
and other such tools allow. This can cause mild confusion, as if the
start of a line in the final form happens to have a * then it will
unexpectedly remove it, but this is a problem shared by those tools too
and the intent is that everyone just use the first form and never need
to worry about it.
|
|
These were only parsed for val specs and scattered clauses, but many
other constructs can be meaningfully documented. Moreover, attaching the
documentation to the SD_aux rather than the FCL_aux etc inside it is
unhelpful since the latter is what the LaTeX backend sees.
Instead, push the documentation down into the non-scattered entity
within the SD_aux (i.e. the FCL_aux / Tu_aux / MCL_aux) when possible,
only leaving it on the SD_aux when they are more like a val spec. This
means that the saildoc for scattered function clauses is now emitted,
without any changes needed to the LaTeX backend.
Also support saildoc on a wider variety of non-scattered constructs, and
slightly simplify aspects of the grammar whilst here.
|
|
|
|
Improve gitignore and documentation a little
|
|
opam pin is useful in the development workflow.
About the rewording: The tests of Sail check the behavior of Sail and
not whether it is installed correctly, because the instructions above
that paragraph don’t install Sail, they just build it.
These circumstances weren’t represented appropriately by the text.
|
|
Both /.gitignore and /lib/coq/.gitignore ignored some files in /lib/coq.
This commit removes /lib/coq/.gitignore and moves all ignore-statements
to /.gitignore . This should simplify the maintenance of gitignore files.
The situation with /test/mono/.gitignore is analogous.
|
|
The "c" tests produce some *.h files that didn’t get ignored. The "coq"
tests also produce some files that weren’t ignored.
|
|
|
|
- add tests for a couple of related rewrites
- accept same range of constants for sign extension in the rewrite as for
the zero extension version (to make the test simpler)
|
|
|
|
|
|
|
|
For example, if a 129-bit capability is given as a 132-bit hex literal
and truncated, this produces a 129-bit binary literal. In isla, this will
keep all of the computation concrete because 129-bit concrete values are
supported.
|
|
Also remove omega workaround that lia doesn't need.
|
|
|
|
|
|
|
|
Can be set by C emulator to control where coverage information is
written
|
|
|
