#
408bf413 |
|
19-Mar-2020 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
lib: Isabelle2020 update Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
|
#
a424d55e |
|
09-Mar-2020 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
licenses: convert license tags to SPDX
|
#
e7fa23ab |
|
13-Nov-2018 |
Edward Pierzchalski <ed.pierzchalski@data61.csiro.au> |
lib: fix up Levity dependency tracking Uses proof body terms to disambiguate the names encoutered in dependency extraction, rather than using (for example) Thm.full_prop_of. The result is that this catches a few more missing dependencies, enough to correctly identify unused lemmas large sessions like CRefine.
|
#
ecc84ffc |
|
22-Oct-2018 |
Edward Pierzchalski <ed.pierzchalski@data61.csiro.au> |
lib: fix up Levity JSON output - Previously printed `~` for negative numbers, which is invalid JSON. Now prints `-`. - Previously the outpout would unconditionally trim 'underscore-number' suffixes. Now uses theory context to determine if it's likely to be an index into a theory list or an existing fact name. - Changed JSON structure to avoid using dynamic names for keys, i.e. from this: { "my_theory_name": {...} } to this: { "theory": "my_theory_name", "content": {...} } This should make processing the output slightly nicer by matching what other tools expect. - Changed JSON structure to consolidate dependencies. Lemmas are no longer special-cased.
|
#
1ae3a8d6 |
|
20-Jun-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
Isabelle2018: Lib update
|
#
6b9d9d24 |
|
09-Jun-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
|
#
00cab83c |
|
27-Jun-2018 |
Japheth Lim <Japheth.Lim@data61.csiro.au> |
lib: fix AutoLevity JSON string encoding
|
#
796887d9 |
|
11-Jul-2017 |
Alejandro Gomez-Londono <alejandro.gomez@nicta.com.au> |
Removes all trailing whitespaces
|
#
92139db6 |
|
25-May-2016 |
Daniel Matichuk <daniel.matichuk@nicta.com.au> |
autolevity: refine tracing apply everywhere to work via Proof module hooks This avoids doing redundant tactic operations at the top-level and lets us trace "by" statements easily.
|
#
4c89bcf2 |
|
20-May-2016 |
Daniel Matichuk <daniel.matichuk@nicta.com.au> |
autolevity: add support for per-apply lemma dependency tracking Also remove at-end theory hook due to unfinished proofs causing issues. Autolevity must be run from a completed session (see lib/AutoLevity_Run). Per-apply dependency tracking requires a small isabelle patch.
|
#
cd21f597 |
|
16-May-2016 |
Daniel Matichuk <daniel.matichuk@nicta.com.au> |
autolevity: make output more JSON compliant
|
#
7553a4e7 |
|
16-May-2016 |
Daniel Matichuk <daniel.matichuk@nicta.com.au> |
autolevity: make output JSON
|
#
df8e65fb |
|
16-May-2016 |
Daniel Matichuk <daniel.matichuk@nicta.com.au> |
autolevity: initial commit with test run on AInvs
|