-
Notifications
You must be signed in to change notification settings - Fork 61
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
5690eb8
commit f1b4e4d
Showing
3 changed files
with
4 additions
and
4 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,4 +1,4 @@ | ||
| <!DOCTYPE html> | ||
| <html xmlns="http://www.w3.org/1999/xhtml"><head><title>ASLRefREADME (herdtools7.ASLRefREADME)</title><link rel="stylesheet" href="../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.1"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="index.html">Up</a> – <a href="index.html">herdtools7</a> » ASLRefREADME</nav><header class="odoc-preamble"><h1 id="getting-started-with-aslref"><a href="#getting-started-with-aslref" class="anchor"></a>Getting started with ASLRef</h1></header><nav class="odoc-toc"><ul><li><a href="#disclaimer">Disclaimer</a></li><li><a href="#installation">Installation</a><ul><li><a href="#pre-requisites">Pre-requisites</a></li><li><a href="#building">Building</a></li><li><a href="#checking">Checking</a></li></ul></li><li><a href="#running">Running</a><ul><li><a href="#basics">Basics</a></li><li><a href="#version-and-type-checking-flags">Version and type-checking flags</a><ul><li><a href="#asl-version">ASL Version</a></li><li><a href="#type-checking">Type-checking</a></li></ul></li><li><a href="#examples">Examples</a></li></ul></li></ul></nav><div class="odoc-content"><h2 id="disclaimer"><a href="#disclaimer" class="anchor"></a>Disclaimer</h2><p>This material covers both ASLv0 (viz, the existing ASL pseudocode language which appears in the Arm Architecture Reference Manual) and ASLv1, a new, experimental, and as yet unreleased version of ASL.</p><p>This material is work in progress, more precisely at pre-Alpha quality as per Arm’s quality standards. In particular, this means that it would be premature to base any production tool development on this material.</p><p>However, any feedback, question, query and feature request would be most welcome; those can be sent to Arm’s Architecture Formal Team Lead Jade Alglave <[email protected]> or by raising issues or PRs to the herdtools7 github repository.</p><h2 id="installation"><a href="#installation" class="anchor"></a>Installation</h2><h3 id="pre-requisites"><a href="#pre-requisites" class="anchor"></a>Pre-requisites</h3><p>The following steps have been tested on Unix.</p><ol><li><p>Install ocaml and opam (ocaml package manager), see <a href="https://ocaml.org/docs/up-and-running#installing-ocaml">the manual</a>. For example on MacOS:</p><pre class="language-bash"><code>$ brew install opam</code></pre></li><li><p>Install dependencies:</p><pre class="language-bash"><code>$ opam install dune menhir zarith</code></pre></li></ol><h3 id="building"><a href="#building" class="anchor"></a>Building</h3><ol><li><p>Clone herdtools7:</p><pre class="language-bash"><code>$ git clone https://github.com/herd/herdtools7.git</code></pre></li><li><p>Build and install into a location <code>$PREFIX</code>:</p><pre class="language-bash"><code>$ make build install PREFIX=$PREFIX</code></pre></li></ol><p>It's done!</p><h3 id="checking"><a href="#checking" class="anchor"></a>Checking</h3><p>If <code>$PREFIX</code> is in your <code>$PATH</code>, the following command should return a similar output:</p><pre class="language-bash"><code>$ aslref --version | ||
| <html xmlns="http://www.w3.org/1999/xhtml"><head><title>ASLRefREADME (herdtools7.ASLRefREADME)</title><link rel="stylesheet" href="../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.2.1"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="index.html">Up</a> – <a href="index.html">herdtools7</a> » ASLRefREADME</nav><header class="odoc-preamble"><h1 id="getting-started-with-aslref"><a href="#getting-started-with-aslref" class="anchor"></a>Getting started with ASLRef</h1></header><nav class="odoc-toc"><ul><li><a href="#disclaimer">Disclaimer</a></li><li><a href="#installation">Installation</a><ul><li><a href="#pre-requisites">Pre-requisites</a></li><li><a href="#building">Building</a></li><li><a href="#checking">Checking</a></li></ul></li><li><a href="#running">Running</a><ul><li><a href="#basics">Basics</a></li><li><a href="#version-and-type-checking-flags">Version and type-checking flags</a><ul><li><a href="#asl-version">ASL Version</a></li><li><a href="#type-checking">Type-checking</a></li></ul></li><li><a href="#examples">Examples</a></li><li><a href="#building-html-pages-locally-from-.mld-files">Building HTML pages locally from .mld files</a></li></ul></li></ul></nav><div class="odoc-content"><h2 id="disclaimer"><a href="#disclaimer" class="anchor"></a>Disclaimer</h2><p>This material covers both ASLv0 (viz, the existing ASL pseudocode language which appears in the Arm Architecture Reference Manual) and ASLv1, a new, experimental, and as yet unreleased version of ASL.</p><p>This material is work in progress, more precisely at pre-Alpha quality as per Arm’s quality standards. In particular, this means that it would be premature to base any production tool development on this material.</p><p>However, any feedback, question, query and feature request would be most welcome; those can be sent to Arm’s Architecture Formal Team Lead Jade Alglave <[email protected]> or by raising issues or PRs to the herdtools7 github repository.</p><h2 id="installation"><a href="#installation" class="anchor"></a>Installation</h2><h3 id="pre-requisites"><a href="#pre-requisites" class="anchor"></a>Pre-requisites</h3><p>The following steps have been tested on Unix.</p><ol><li><p>Install ocaml and opam (ocaml package manager), see <a href="https://ocaml.org/docs/up-and-running#installing-ocaml">the manual</a>. For example on MacOS:</p><pre class="language-bash"><code>$ brew install opam</code></pre></li><li><p>Install dependencies:</p><pre class="language-bash"><code>$ opam install dune menhir zarith</code></pre></li></ol><h3 id="building"><a href="#building" class="anchor"></a>Building</h3><ol><li><p>Clone herdtools7:</p><pre class="language-bash"><code>$ git clone https://github.com/herd/herdtools7.git</code></pre></li><li><p>Build and install into a location <code>$PREFIX</code>:</p><pre class="language-bash"><code>$ make build install PREFIX=$PREFIX</code></pre></li></ol><p>It's done!</p><h3 id="checking"><a href="#checking" class="anchor"></a>Checking</h3><p>If <code>$PREFIX</code> is in your <code>$PATH</code>, the following command should return a similar output:</p><pre class="language-bash"><code>$ aslref --version | ||
| aslref version 7.56+03 rev 7aa9d1f3cee2598ec64f14372f210e008ac5510f</code></pre><p>Please note that building herdtools7 depends on the installation path <code>$PREFIX</code>. If you want to move your installation from <code>$OLD_PREFIX</code> to <code>$NEW_PREFIX</code>, please use:</p><pre class="language-bash"><code>make uninstall PREFIX=$OLD_PREFIX | ||
| make build install PREFIX=$NEW_PREFIX</code></pre><h2 id="running"><a href="#running" class="anchor"></a>Running</h2><h3 id="basics"><a href="#basics" class="anchor"></a>Basics</h3><p>If <code>my-test.asl</code> contains a valid ASL program returning 0, the tool <code>aslref</code> does not print anything and exit with code 0.</p><pre class="language-bash"><code>$ aslref my-test.asl</code></pre><h3 id="version-and-type-checking-flags"><a href="#version-and-type-checking-flags" class="anchor"></a>Version and type-checking flags</h3><p>For a complete reference of arguments, see <code>aslref --help</code>.</p><h4 id="asl-version"><a href="#asl-version" class="anchor"></a>ASL Version</h4><p>To use the ASLv0 parser, use the <code>-0</code> flag.</p><p>The default parser is the ASLv1, but you can still specify it with <code>-1</code>.</p><h4 id="type-checking"><a href="#type-checking" class="anchor"></a>Type-checking</h4><p>There are currently three possible type-checking settings, listed here from the strongest to the weakest:</p><ol><li><code>--type-check-strict</code> fails on the first error encountered while type-checking the program. This is the default setting for ASLv1.</li><li><code>--type-check-warn</code> logs every error on the standard error output, but does not fail on any of them. The program might not be able to run through the interpreter if the type-checking phase failed.</li><li><code>--no-type-check</code> only performs minimal type-inference. Tries to fail as little as possible. This is the default for ASLv0.</li></ol><h3 id="examples"><a href="#examples" class="anchor"></a>Examples</h3><p>You can find examples of ASLv1 programs that <code>aslref</code> supports in <a href="https://github.com/herd/herdtools7/tree/master/asllib/tests/asl/required"><code>herdtools7/asllib/tests/asl/required</code></a>.</p></div></body></html> | ||
| make build install PREFIX=$NEW_PREFIX</code></pre><h2 id="running"><a href="#running" class="anchor"></a>Running</h2><h3 id="basics"><a href="#basics" class="anchor"></a>Basics</h3><p>If <code>my-test.asl</code> contains a valid ASL program returning 0, the tool <code>aslref</code> does not print anything and exit with code 0.</p><pre class="language-bash"><code>$ aslref my-test.asl</code></pre><h3 id="version-and-type-checking-flags"><a href="#version-and-type-checking-flags" class="anchor"></a>Version and type-checking flags</h3><p>For a complete reference of arguments, see <code>aslref --help</code>.</p><h4 id="asl-version"><a href="#asl-version" class="anchor"></a>ASL Version</h4><p>To use the ASLv0 parser, use the <code>-0</code> flag.</p><p>The default parser is the ASLv1, but you can still specify it with <code>-1</code>.</p><h4 id="type-checking"><a href="#type-checking" class="anchor"></a>Type-checking</h4><p>There are currently three possible type-checking settings, listed here from the strongest to the weakest:</p><ol><li><code>--type-check-strict</code> fails on the first error encountered while type-checking the program. This is the default setting for ASLv1.</li><li><code>--type-check-warn</code> logs every error on the standard error output, but does not fail on any of them. The program might not be able to run through the interpreter if the type-checking phase failed.</li><li><code>--no-type-check</code> only performs minimal type-inference. Tries to fail as little as possible. This is the default for ASLv0.</li></ol><h3 id="examples"><a href="#examples" class="anchor"></a>Examples</h3><p>You can find examples of ASLv1 programs that <code>aslref</code> supports in <a href="https://github.com/herd/herdtools7/tree/master/asllib/tests/asl/required"><code>herdtools7/asllib/tests/asl/required</code></a>.</p><h3 id="building-html-pages-locally-from-.mld-files"><a href="#building-html-pages-locally-from-.mld-files" class="anchor"></a>Building HTML pages locally from .mld files</h3><p>In the directory <code>herdtools7/</code>:</p><ol><li><p>Run:</p><pre class="language-bash"><code>$ dune build @doc</code></pre></li></ol><ol><li>Open <code>_build/default/_doc/_html/herdtools7/aslref.html</code></li></ol></div></body></html> |
Large diffs are not rendered by default.
Oops, something went wrong.
Oops, something went wrong.