sail/lib/isabelle, branch sail2 Formal specification language for ISAs Make Isabelle lemma generation work with grouped regstate 2020-05-13T16:04:50+00:00 Thomas Bauereiss 2020-05-09T21:10:49+00:00 336522767a1c3b564fd4798851993afef9f629ed 






Update location of sail2_instr_kinds.lem
2019-11-14T17:06:57+00:00

Robert Norton

2019-11-14T17:02:07+00:00

c4a5c2526259676cadb9b66d3a9d37021e9fd3d8












Perform isabelle check only when heap-img rule is used to avoid calling opam (which might not be present).
2019-11-14T17:01:57+00:00

Robert Norton

2019-11-14T17:01:57+00:00

9dfad153b1305fa14b070a80104bc2cc7f2a974a












Remove generated TeX file
2019-05-08T10:46:11+00:00

Thomas Bauereiss

2019-05-08T10:45:45+00:00

611748f32de5269eb3d56bb3098cf07c9a89a0ba












Patch up a couple of Isabelle proofs due to memory interface changes
2019-05-07T10:01:55+00:00

Brian Campbell

2019-05-07T10:01:55+00:00

326e97e2ecaafaae75b841999fc94eed34e9a841












More read/write function updates
2019-04-25T16:13:29+00:00

Brian Campbell

2019-04-25T16:13:29+00:00

911153ffefdfb090557c6dfcc5a5143419c34f56












Basic loop termination measures for Coq
2019-04-15T11:08:28+00:00

Brian Campbell

2019-04-15T11:08:28+00:00

1f421b865a87a161a82550443a0cf39aa2642d9c

Currently only supports pure termination measures for loops with effects.

The user syntax uses separate termination measure declarations, as in the
previous recursive termination measures, which are rewritten into the
loop AST nodes before type checking (because it would be rather difficult
to calculate the correct environment to type check the separate declaration
in).





Currently only supports pure termination measures for loops with effects.

The user syntax uses separate termination measure declarations, as in the
previous recursive termination measures, which are rewritten into the
loop AST nodes before type checking (because it would be rather difficult
to calculate the correct environment to type check the separate declaration
in).







Build Isabelle heap image instead of just running session
2019-01-31T14:42:29+00:00

Thomas Bauereiss

2019-01-31T14:42:29+00:00

ccc11a48d38f634f98853fe940d1d484bb7b7fe8












Merge branch 'monads' into asl_flow2
2019-01-31T13:42:24+00:00

Thomas Bauereiss

2019-01-31T13:42:24+00:00

2cc9a0795a571140fa039bdc9a02e70d47f3c7cb












Don't let "make" fail unnecessarily in lib/isabelle
2019-01-23T16:29:49+00:00

Thomas Bauereiss

2019-01-23T16:29:49+00:00

1951607813f73688297840fc4ae4b3059b7528c5

Only check for availability of Lem library if actually trying to build
an Isabelle heap image.





Only check for availability of Lem library if actually trying to build
an Isabelle heap image.