#
2e8cf15b |
|
19-Mar-2020 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
lib + proof: Isabelle2020 Method.NO_CONTEXT_TACTIC rename Method.NO_CONTEXT_TACTIC -> NO_CONTEXT_TACTIC Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
|
#
408bf413 |
|
19-Mar-2020 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
lib: Isabelle2020 update Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
|
#
a6ffe216 |
|
23-Jul-2020 |
Corey Lewis <Corey.Lewis@data61.csiro.au> |
lib: improve crunch warning message Refactor crunch to separately specify whether crunch_simps or crunch_wps might be useful instead of printing one combined message. Signed-off-by: Corey Lewis <Corey.Lewis@data61.csiro.au>
|
#
dad926df |
|
23-Jul-2020 |
Corey Lewis <Corey.Lewis@data61.csiro.au> |
lib: improve crunch warning message Change crunch to only warn when crunch_simps or crunch_wps can make progress on the first goal. Previously it would try on all remaining subgoals, which led to spurious warnings when schematic postconditions could be unified incorrectly. Signed-off-by: Corey Lewis <Corey.Lewis@data61.csiro.au>
|
#
a424d55e |
|
09-Mar-2020 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
licenses: convert license tags to SPDX
|
#
170e8109 |
|
25-Feb-2020 |
Corey Lewis <corey.lewis@data61.csiro.au> |
lib: refactor crunch warning messages to handle functions with multiple patterns Crunch would print spurious warning messages when using a rule with multiple premises. By default, crunch generates a rule like that when applied to functions with multiple non-trivial patterns.
|
#
d21ea9da |
|
29-Jan-2020 |
Corey Lewis <corey.lewis@data61.csiro.au> |
lib: reimplement crunch call stack feature so that it works when proofs fail. This stopped working when crunch was changed to fork proofs.
|
#
5120e351 |
|
04-Nov-2019 |
Corey Lewis <corey.lewis@data61.csiro.au> |
lib: improve wp tracing When tracing wp can now print the instantiated version of the rules being used. It also says which set each used rule is from.
|
#
41b48636 |
|
14-Oct-2019 |
Corey Lewis <corey.lewis@data61.csiro.au> |
lib: add a warning if crunch fails and top-level constant is being ignored
|
#
b6689ba3 |
|
29-Aug-2019 |
Corey Lewis <corey.lewis@data61.csiro.au> |
lib: restrict safe in core crunch tactic so that we can avoid passing around the index
|
#
8c3e7aa1 |
|
22-Jul-2019 |
Corey Lewis <corey.lewis@data61.csiro.au> |
lib: make wp_cases_tac subgoal aware
|
#
96588daf |
|
17-Jul-2019 |
Corey Lewis <corey.lewis@data61.csiro.au> |
lib: improve message printing for crunch and wp, and refactor common printing functions
|
#
9a9c6320 |
|
17-Jul-2019 |
Corey Lewis <corey.lewis@data61.csiro.au> |
lib: various crunch improvements The main one is that crunch now uses wpsimp when determining whether a goal can already be solved, instead of just wp. Crunch can also now use wps when proving a goal and will now always ignore a constant if told to, even if it is the top-level constant being crunched.
|
#
f757e0ca |
|
06-May-2019 |
Corey Lewis <corey.lewis@data61.csiro.au> |
lib: wp cleanup and parser improvements The main visible change is from wp_trace', 'wp_once' and 'wp_once_trace' to 'wp (trace)', 'wp (once)' and 'wp (once, trace)'. The option for printing a warning for unused supplied wp rules has also been removed.
|
#
95ddba3d |
|
14-Apr-2019 |
Corey Lewis <corey.lewis@data61.csiro.au> |
lib: improve the parser for crunch. The main benefit of this is that everything in crunch is now ctrl clickable. As an added benefit, supplied rules can now be modified by attributes when needed.
|
#
ea7c58bf |
|
23-Jul-2018 |
Thomas Sewell <Thomas.Sewell@data61.csiro.au> |
lib/crunch: use induct package. Discard some magic that was done to instantiate an induction rule, and instead use the existing Induct_Tacs package to apply induction rules, which seems to be successful more often.
|
#
d77d31a7 |
|
03-Jun-2018 |
Corey Lewis <corey.lewis@data61.csiro.au> |
lib: Refactor crunch so that it can be used for both the nondet monad and the trace monad
|
#
c686d6e7 |
|
07-Jun-2018 |
Corey Lewis <corey.lewis@data61.csiro.au> |
lib: Make Crunch more effective at applying supplied rules
|
#
dceb2692 |
|
05-Jun-2018 |
Corey Lewis <corey.lewis@data61.csiro.au> |
lib: Add a warning to crunch if it does not do anything
|
#
55d20591 |
|
13-Mar-2018 |
Corey Lewis <corey.lewis@data61.csiro.au> |
lib: improved crunch The main aim of this is for crunch to make consistent decisions about whether to prove new rules. If any rules in the wp set can be used to directly solve the goal crunch is working on, then crunch will just use it. Other changes include: - crunch_ignore works properly inside locales again. - if a rule already exists with the specific name crunch is going to use, but that rule does not solve the goal crunch is working on then crunch will now error. - if crunch fails to prove a goal it will now output a warning if adding crunch_simps or crunch_wps would allow it to make more progess.
|
#
a70aeda3 |
|
21-Jan-2018 |
Thomas Sewell <Thomas.Sewell@data61.csiro.au> |
lib: Datatype_Schematic and WPFix. Add two new tactics/methods which can fix common painful problems with schematic variables. Method datatype_schem improves unification outcomes, by making judicious use of selectors like fst/snd/the/hd to bring variables into scope, and also using a wrapper to avoid singleton constants like True being captured needlessly by unification. Method wpfix uses strengthen machinery to instantiate rogue postcondition schematics to True and to split precondition schematics that are shared across different sites.
|
#
d2f38a0a |
|
31-Jan-2018 |
Thomas Sewell <Thomas.Sewell@data61.csiro.au> |
lib: Add multi-crunch command 'crunches'. It's just a parser tweak for crunch, and runs multiple crunch commands with the same sections (wps, ignores, etc). Also update the comments a little, and move them closer to the anchor of command clicks (the @{command_keyword} antiquotation).
|
#
5152952a |
|
31-Jan-2018 |
Thomas Sewell <Thomas.Sewell@data61.csiro.au> |
lib: Cleanup in crunch-cmd.ML Mostly syntactic. Ensure less debug messages are generated unconditionally.
|
#
184d6b70 |
|
09-Oct-2017 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
remove most tab characters
|
#
30122b5d |
|
10-Nov-2016 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
Isabelle2016-1: update to new ML API Update references to renamed ML constants; supply default arguments to functions with additional parameters; etc.
|
#
41d4aa4f |
|
25-Oct-2016 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
Isabelle2016-1: update references to renamed constants and facts
|
#
9a1ec71a |
|
23-Aug-2016 |
Thomas Sewell <Thomas.Sewell@nicta.com.au> |
Refactor of crunch. Substantial adjustments to crunch. Main user changes are: - 'lift' and 'unfold' mechanisms replaced by more general 'rule'. - some more 'ignores' standardised. - crunch has a more principled overall design: + discover crunch rule * provided or by definition extraction + recurse according to rule + prove goal based on rule, recursive discoveries, standard tactic * wp/simp adjustments tweak tactic
|
#
670d1c11 |
|
02-May-2016 |
Daniel Matichuk <daniel.matichuk@nicta.com.au> |
arch_split: added optional definition override for crunch. Reduced qualification commands to minimal required set.
|
#
0805d9f9 |
|
21-Jan-2016 |
Daniel Matichuk <daniel.matichuk@nicta.com.au> |
make crunch fork proofs
|
#
8f9761ab |
|
21-Jan-2016 |
Daniel Matichuk <daniel.matichuk@nicta.com.au> |
make crunch prove in parallel when possible
|
#
b7563eb7 |
|
11-Jan-2016 |
Daniel Matichuk <daniel.matichuk@nicta.com.au> |
fix lib for isabelle 2016
|
#
f0ce95aa |
|
22-Nov-2015 |
Corey Lewis <corey.lewis@nicta.com.au> |
Fix wp_del for crunch.
|
#
a2cc6ab3 |
|
11-Nov-2015 |
Corey Lewis <corey.lewis@nicta.com.au> |
Added wp_del and simp_del arguments to crunch.
|
#
f2cfeb2a |
|
16-May-2015 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
lib: fewer warnings in crunch and wps
|
#
12fa8686 |
|
16-May-2015 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
fewer warnings
|
#
17826f9b |
|
18-Apr-2015 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
more Isabelle2015 update; AInvs up to (excluding) Syscall_AI also includes some global replacements
|
#
0547cb70 |
|
15-Sep-2014 |
David Greenaway <david.greenaway@nicta.com.au> |
crunch: Reduce tracing messages, use "writeln" instead of "tracing". Excessinve tracing messages cause jEdit to pause, waiting for the user to click "Show more tracing output. We eliminate the debugging tracing messages by default, and use "writeln" instead for the remainder. ("writeln" doesn't cause jEdit to pause.)
|
#
e8d1ed6d |
|
09-Aug-2014 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
ported lib/* theories to Isabelle2014-RC0
|
#
1af1d2b6 |
|
08-Aug-2014 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
some of the global Isabelle2014 renames option_case -> case_option sum_case -> case_sum prod_case -> case_prod Option.set -> set_option Option.map -> map_option option_rel -> rel_option list_all2_def -> list_all2_iff map.simps -> list.map tl.simps -> list.sel(2-3) the.simps -> option.sel
|
#
50dda770 |
|
22-Jul-2014 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
comment cleanup
|
#
2a03e81d |
|
14-Jul-2014 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
Import release snapshot.
|