sail/lib, branch sail2

Fix lemma for current HOL4

2021-03-24T18:11:08+00:00

(should also work for older versions)

Don't use x86 intrinsics

2021-01-06T13:11:53+00:00

Fix some cases when monomorphising vectors containing variable-length bitvectors

2021-01-05T14:36:21+00:00

Add write tag primitive

2020-11-19T18:09:15+00:00

Support C coverage when sail_exit is used

2020-10-14T21:46:27+00:00

pass pointer to g_elf_entry to get the ELF entry

2020-10-01T07:14:38+00:00

Tweak Coq proof to avoid incompatibility with Iris

2020-09-30T16:26:09+00:00

(in the previous proof script the intuition tactic found a strange proof
involving a type-level dependent pair that imposed an unnecessary
universe constraint, this doesn't)

Merge some of the gitignore files

2020-09-12T21:00:19+00:00

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.

Fix typo a mono_rewrites definition

2020-09-07T12:40:24+00:00

- 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)

Correct external declaration in mono_rewrites

2020-09-07T12:40:24+00:00