Skip to content
This repository has been archived by the owner on Aug 8, 2020. It is now read-only.

Commit

Permalink
Tweak record of Lem version in readmes
Browse files Browse the repository at this point in the history
  • Loading branch information
xrchz committed Jan 14, 2019
1 parent 071dd6d commit 89ac706
Show file tree
Hide file tree
Showing 3 changed files with 11 additions and 13 deletions.
6 changes: 3 additions & 3 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -68,9 +68,9 @@ Auxiliary files providing glue between a standard HOL installation
and what we want to use for CakeML development.

[semantics](semantics):
The definition of the CakeML language. The definition is (mostly)
expressed in [Lem](http://www.cs.kent.ac.uk/~sao/lem), but the
generated HOL is also included. The directory includes definitions of:
The definition of the CakeML language. The definition is (mostly) expressed in
[Lem](https://www.cl.cam.ac.uk/~pes20/lem), but the generated HOL is included.
The directory includes definitions of:
- the concrete syntax,
- the abstract syntax,
- big step semantics (both functional and relational),
Expand Down
9 changes: 4 additions & 5 deletions semantics/README.md
Original file line number Diff line number Diff line change
@@ -1,15 +1,14 @@
The definition of the CakeML language. The definition is (mostly)
expressed in [Lem](http://www.cs.kent.ac.uk/~sao/lem), but the
generated HOL is also included. The directory includes definitions of:
The definition of the CakeML language. The definition is (mostly) expressed in
[Lem](https://www.cl.cam.ac.uk/~pes20/lem), but the generated HOL is included.
The directory includes definitions of:
- the concrete syntax,
- the abstract syntax,
- big step semantics (both functional and relational),
- a small step semantics,
- the semantics of FFI calls, and,
- the type system.

The script files in this directory were generated using Lem commit 194778e.
If you use a newer lem commit to generate the script files, please update this.
The Lem version used: rems-project/lem@194778e97d1e9a41ebbe34a8e4d5fb2d10395ba7

[addancs.sml](addancs.sml):
A script to add a set_grammar_ancestry line to a generated Script.sml file.
Expand Down
9 changes: 4 additions & 5 deletions semantics/readmePrefix
Original file line number Diff line number Diff line change
@@ -1,12 +1,11 @@
The definition of the CakeML language. The definition is (mostly)
expressed in [Lem](http://www.cs.kent.ac.uk/~sao/lem), but the
generated HOL is also included. The directory includes definitions of:
The definition of the CakeML language. The definition is (mostly) expressed in
[Lem](https://www.cl.cam.ac.uk/~pes20/lem), but the generated HOL is included.
The directory includes definitions of:
- the concrete syntax,
- the abstract syntax,
- big step semantics (both functional and relational),
- a small step semantics,
- the semantics of FFI calls, and,
- the type system.

The script files in this directory were generated using Lem commit 194778e.
If you use a newer lem commit to generate the script files, please update this.
The Lem version used: rems-project/lem@194778e97d1e9a41ebbe34a8e4d5fb2d10395ba7

0 comments on commit 89ac706

Please sign in to comment.