| #
4886a476 |
|
21-Jun-2017 |
blanchet <none@none> |
added -d option to Mirabelle
|
| #
ea36273b |
|
07-Aug-2012 |
boehmes <none@none> |
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
|
| #
2926c362 |
|
02-May-2012 |
wenzelm <none@none> |
more robust wrt. spaces in directory names;
|
| #
d9b328a8 |
|
02-May-2012 |
wenzelm <none@none> |
back to "Tools" in conformance with toplevel Isabelle layout (cf. 3fabf352243e, 15f4309bb9eb);
|
| #
1204e96e |
|
24-Apr-2012 |
sultana <none@none> |
reversed Tools to Actions Mirabelle renaming;
--HG--
rename : src/HOL/Mirabelle/Actions/mirabelle.ML => src/HOL/Mirabelle/Tools/mirabelle.ML
rename : src/HOL/Mirabelle/Actions/mirabelle_arith.ML => src/HOL/Mirabelle/Tools/mirabelle_arith.ML
rename : src/HOL/Mirabelle/Actions/mirabelle_metis.ML => src/HOL/Mirabelle/Tools/mirabelle_metis.ML
rename : src/HOL/Mirabelle/Actions/mirabelle_quickcheck.ML => src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML
rename : src/HOL/Mirabelle/Actions/mirabelle_refute.ML => src/HOL/Mirabelle/Tools/mirabelle_refute.ML
rename : src/HOL/Mirabelle/Actions/mirabelle_sledgehammer.ML => src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
rename : src/HOL/Mirabelle/Actions/mirabelle_sledgehammer_filter.ML => src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
|
| #
33b91d46 |
|
14-Apr-2012 |
sultana <none@none> |
Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action
|
| #
21a667e2 |
|
14-Apr-2012 |
sultana <none@none> |
Mirabelle now gives usage info when no arguments given
|
| #
a5ce7279 |
|
14-Apr-2012 |
sultana <none@none> |
switched from using sed to perl in mirabelle tool
|
| #
9f573af9 |
|
14-Apr-2012 |
sultana <none@none> |
renamed mirabelle Tools directory to Actions, to make consistent with 'usage' description;
--HG--
rename : src/HOL/Mirabelle/Tools/mirabelle.ML => src/HOL/Mirabelle/Actions/mirabelle.ML
rename : src/HOL/Mirabelle/Tools/mirabelle_arith.ML => src/HOL/Mirabelle/Actions/mirabelle_arith.ML
rename : src/HOL/Mirabelle/Tools/mirabelle_metis.ML => src/HOL/Mirabelle/Actions/mirabelle_metis.ML
rename : src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML => src/HOL/Mirabelle/Actions/mirabelle_quickcheck.ML
rename : src/HOL/Mirabelle/Tools/mirabelle_refute.ML => src/HOL/Mirabelle/Actions/mirabelle_refute.ML
rename : src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML => src/HOL/Mirabelle/Actions/mirabelle_sledgehammer.ML
rename : src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML => src/HOL/Mirabelle/Actions/mirabelle_sledgehammer_filter.ML
|
| #
4498df6e |
|
07-Mar-2012 |
sultana <none@none> |
added Mirabelle action info in its log file; tuned;
|
| #
837fc776 |
|
23-Mar-2011 |
krauss <none@none> |
replace hardwired MIRABELLE_OUTPUT_PATH by temporary directory derived from ISABELLE_TMP_PREFIX and $$ -- old behaviour can be achieved by manually setting MIRABELLE_OUTPUT_PATH
|
| #
b5475dc3 |
|
20-Mar-2011 |
krauss <none@none> |
propagate mirabelle failures properly;
flatten obscure return code semantics of Perl system command to 0/1
|
| #
637b1c78 |
|
06-Dec-2010 |
bulwahn <none@none> |
correcting usage documentation in mirabelle tool
|
| #
88a0057f |
|
08-Dec-2009 |
boehmes <none@none> |
also consider the fully-typed version of metis for Mirabelle measurements
|
| #
ac3957b7 |
|
27-Oct-2009 |
boehmes <none@none> |
included description for sledgehammer options in Mirabelle script
|
| #
d464349e |
|
02-Sep-2009 |
boehmes <none@none> |
moved Mirabelle from HOL/Tools to HOL,
added session HOL-Mirabelle
--HG--
rename : src/HOL/Tools/Mirabelle/Mirabelle.thy => src/HOL/Mirabelle/Mirabelle.thy
rename : src/HOL/Tools/Mirabelle/Tools/mirabelle.ML => src/HOL/Mirabelle/Tools/mirabelle.ML
rename : src/HOL/Tools/Mirabelle/Tools/mirabelle_arith.ML => src/HOL/Mirabelle/Tools/mirabelle_arith.ML
rename : src/HOL/Tools/Mirabelle/Tools/mirabelle_metis.ML => src/HOL/Mirabelle/Tools/mirabelle_metis.ML
rename : src/HOL/Tools/Mirabelle/Tools/mirabelle_quickcheck.ML => src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML
rename : src/HOL/Tools/Mirabelle/Tools/mirabelle_refute.ML => src/HOL/Mirabelle/Tools/mirabelle_refute.ML
rename : src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML => src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
rename : src/HOL/Tools/Mirabelle/doc/options.txt => src/HOL/Mirabelle/doc/options.txt
rename : src/HOL/Tools/Mirabelle/etc/settings => src/HOL/Mirabelle/etc/settings
rename : src/HOL/Tools/Mirabelle/lib/Tools/mirabelle => src/HOL/Mirabelle/lib/Tools/mirabelle
rename : src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl => src/HOL/Mirabelle/lib/scripts/mirabelle.pl
|
| #
22bc24a6 |
|
05-Sep-2009 |
boehmes <none@none> |
Mirabelle: command-line action options may either be key=value or just key
|
| #
eb02c671 |
|
05-Sep-2009 |
boehmes <none@none> |
added initialization and cleanup of actions,
added option to suppress Isabelle output,
sledgehammer action produces its own report (no need for additional perl script)
|