Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -120 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
Thu, 26 Jun 2014 13:33:08 +0200 blanchet adaptive k-NN file | diff | annotate
Tue, 24 Jun 2014 15:08:19 +0200 blanchet optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct) file | diff | annotate
Tue, 24 Jun 2014 14:56:08 +0200 blanchet minor table access optimization file | diff | annotate
Tue, 24 Jun 2014 12:36:45 +0200 blanchet optimize log file | diff | annotate
Tue, 24 Jun 2014 12:35:57 +0200 blanchet enable TF-IDF file | diff | annotate
Tue, 24 Jun 2014 12:35:49 +0200 blanchet added another experimental engine file | diff | annotate
Tue, 24 Jun 2014 12:35:43 +0200 blanchet tweaked experimental setup file | diff | annotate
Tue, 24 Jun 2014 08:19:58 +0200 blanchet use strings to communicate with external process, to ease debugging file | diff | annotate
Tue, 24 Jun 2014 08:19:55 +0200 blanchet added experimental MaSh engine file | diff | annotate
Fri, 20 Jun 2014 09:55:31 +0200 blanchet changed default MaSh parameters based on (in vitro) evaluation file | diff | annotate
Wed, 18 Jun 2014 17:42:24 +0200 blanchet more MaSh engine variations, for evaluations file | diff | annotate
Wed, 18 Jun 2014 17:42:24 +0200 blanchet split parameter into two file | diff | annotate
Wed, 18 Jun 2014 15:23:40 +0200 blanchet more generous formula -- there are lots of duplicates out there file | diff | annotate
Wed, 18 Jun 2014 14:19:42 +0200 blanchet automatically learn MaSh facts also in 'blocking' mode file | diff | annotate
Mon, 02 Jun 2014 11:59:50 +0200 blanchet add option to keep duplicates, for more precise evaluation of relevance filters file | diff | annotate
Fri, 30 May 2014 16:00:54 +0200 blanchet made 'Kuehlwein-style' be really like Python code, we now think file | diff | annotate
Fri, 30 May 2014 15:15:41 +0200 blanchet make SML code closer to Python code when 'nb_kuehlwein_style' is true file | diff | annotate
Fri, 30 May 2014 14:43:06 +0200 blanchet added sleep to give time for the server to shut down -- this is a hack, but it's only in experimental code that will hopefully soon go away file | diff | annotate
Fri, 30 May 2014 12:27:51 +0200 blanchet added another way of invoking Python code, for experiments file | diff | annotate
Fri, 30 May 2014 12:27:51 +0200 blanchet make SML naive Bayes closer to Python version file | diff | annotate
Fri, 30 May 2014 12:27:51 +0200 blanchet more work on exporter file | diff | annotate
Fri, 30 May 2014 12:27:51 +0200 blanchet extend exporter with new versions of MaSh file | diff | annotate
Wed, 28 May 2014 17:42:36 +0200 blanchet more generous max number of suggestions, for more safety file | diff | annotate
Wed, 28 May 2014 17:42:34 +0200 blanchet changed MaSh to use SML version instead of Python version of naive Bayes by default (i.e. if MASH=yes in the settings, or 'fact_filter=mash' with no other explicit setting) file | diff | annotate
Wed, 28 May 2014 17:42:33 +0200 blanchet export more ML functions, for experimentation file | diff | annotate
Wed, 28 May 2014 14:02:49 +0200 blanchet disabled IDF for now -- empirical evidence points the wrong way (as usual) file | diff | annotate
Wed, 28 May 2014 13:31:44 +0200 blanchet tuning file | diff | annotate
Wed, 28 May 2014 13:02:47 +0200 blanchet tuning file | diff | annotate
Wed, 28 May 2014 12:34:26 +0200 blanchet optimized computation file | diff | annotate
Wed, 28 May 2014 10:04:28 +0200 blanchet enabled IDF for naive Bayes ML file | diff | annotate
Wed, 28 May 2014 10:03:14 +0200 blanchet tuning file | diff | annotate
Wed, 28 May 2014 09:44:14 +0200 blanchet repaired subscript problem in SML kNN file | diff | annotate
Wed, 28 May 2014 09:38:39 +0200 blanchet tuning file | diff | annotate
Wed, 28 May 2014 03:10:30 +0200 blanchet always remove duplicates in meshing + use weights for Naive Bayes file | diff | annotate
Tue, 27 May 2014 17:48:11 +0200 blanchet updated naive Bayes file | diff | annotate
Mon, 26 May 2014 14:15:48 +0200 blanchet renamed 'MaSh' option file | diff | annotate
Fri, 23 May 2014 14:12:20 +0200 blanchet automatically reload state file when it changes on disk file | diff | annotate
Thu, 22 May 2014 14:27:43 +0200 blanchet avoid slow inspection of proof terms now that dependencies are stored in 'state' file | diff | annotate
Thu, 22 May 2014 13:46:49 +0200 blanchet properly mark relearns as dirty file | diff | annotate
Thu, 22 May 2014 13:07:53 +0200 blanchet disable weights that cause more harm than they help in kNN file | diff | annotate
Thu, 22 May 2014 13:07:52 +0200 blanchet add self dependency to naive Bayes file | diff | annotate
Thu, 22 May 2014 13:07:51 +0200 blanchet make MaSh Python the default when passing 'fact_filter = mash' without enabling the 'maSh' Isabelle system option file | diff | annotate
Thu, 22 May 2014 04:12:06 +0200 blanchet reverted '|' features in MaSh -- these sounded like a good idea but never really worked file | diff | annotate
Thu, 22 May 2014 03:29:35 +0200 blanchet until naive Bayes supports weights, don't incorporate 'extra' low-weight features file | diff | annotate
Wed, 21 May 2014 14:09:43 +0200 blanchet added comment file | diff | annotate
Tue, 20 May 2014 22:28:44 +0200 blanchet added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN) file | diff | annotate
Tue, 20 May 2014 22:28:08 +0200 blanchet added Isabelle system option 'mash' file | diff | annotate
Tue, 20 May 2014 16:31:39 +0200 blanchet more flexible environment variable file | diff | annotate
Tue, 20 May 2014 16:11:37 +0200 blanchet tuning file | diff | annotate
Tue, 20 May 2014 09:57:10 +0200 blanchet implemented MaSh/SML hints file | diff | annotate
Tue, 20 May 2014 09:38:39 +0200 blanchet better way to take invisible facts into account than 'island' business file | diff | annotate
Tue, 20 May 2014 02:47:23 +0200 blanchet cleaner handling of learned proofs file | diff | annotate
Tue, 20 May 2014 00:13:31 +0200 blanchet implemented learning of single proofs in SML MaSh file | diff | annotate
Mon, 19 May 2014 23:43:53 +0200 blanchet take weights into consideration in knn file | diff | annotate
Mon, 19 May 2014 23:43:53 +0200 blanchet added SML implementation of MaSh file | diff | annotate
Mon, 19 May 2014 23:43:53 +0200 blanchet started work on MaSh/SML file | diff | annotate
Mon, 19 May 2014 23:43:53 +0200 blanchet tune file | diff | annotate
Mon, 19 May 2014 23:43:53 +0200 blanchet store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution file | diff | annotate
Mon, 19 May 2014 13:53:58 +0200 blanchet hide more consts to beautify documentation file | diff | annotate
Thu, 27 Mar 2014 17:12:40 +0100 wenzelm clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler; file | diff | annotate
Sat, 22 Mar 2014 18:19:57 +0100 wenzelm more antiquotations; file | diff | annotate
Fri, 21 Feb 2014 00:09:56 +0100 blanchet adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec' file | diff | annotate
Mon, 03 Feb 2014 15:33:18 +0100 blanchet tuning file | diff | annotate
Fri, 31 Jan 2014 10:23:32 +0100 blanchet renamed many Sledgehammer ML files to clarify structure file | diff | annotate
Fri, 31 Jan 2014 10:23:32 +0100 blanchet renamed ML file file | diff | annotate
Thu, 19 Dec 2013 13:43:21 +0100 blanchet made timeouts in Sledgehammer not be 'option's -- simplified lots of code file | diff | annotate
Wed, 18 Dec 2013 16:50:14 +0100 blanchet tuning file | diff | annotate
Mon, 09 Dec 2013 04:44:59 +0100 blanchet disable generalization in MaSh until it is shown to help file | diff | annotate
Mon, 09 Dec 2013 04:03:30 +0100 blanchet generate problems with type classes file | diff | annotate
Mon, 09 Dec 2013 04:03:30 +0100 blanchet more reasonable default weight file | diff | annotate
Tue, 19 Nov 2013 18:34:04 +0100 blanchet tuning file | diff | annotate
Thu, 14 Nov 2013 15:57:48 +0100 blanchet have MaSh support nameless facts (i.e. proofs) and use that support file | diff | annotate
Fri, 18 Oct 2013 00:05:31 +0200 blanchet make sure add: doesn't add duplicates, and works for [no_atp] facts file | diff | annotate
Thu, 17 Oct 2013 20:49:19 +0200 blanchet generate a comment storing the goal nickname in "learn_prover" file | diff | annotate
Thu, 17 Oct 2013 20:20:53 +0200 blanchet clarified message file | diff | annotate
Thu, 17 Oct 2013 02:29:49 +0200 blanchet choose facts to reprove more randomly, to avoid getting stuck with impossible problems at first file | diff | annotate
Thu, 17 Oct 2013 01:04:00 +0200 blanchet if slicing is disabled, don't enforce last slice's "max_facts", but rather the maximum "max_facts" file | diff | annotate
Thu, 17 Oct 2013 01:03:59 +0200 blanchet remove overloading of "max_facts" -- it already controls the number of facts passed to ATPs for 'learn_prover' file | diff | annotate
Tue, 15 Oct 2013 16:14:52 +0200 blanchet improved duplicate detection in "build_name_tables" by ensuring that the earliest occurrence of a duplicate (if it exists) gets picked as the canonical instance file | diff | annotate
Sun, 13 Oct 2013 21:36:26 +0200 blanchet more prominent MaSh errors file | diff | annotate
Thu, 10 Oct 2013 08:23:57 +0200 blanchet repaired confusion between the stated and effective fact filter -- the mismatch could result in "Match" exceptions file | diff | annotate
Thu, 10 Oct 2013 01:17:37 +0200 blanchet simplify fudge factor code file | diff | annotate
Wed, 09 Oct 2013 16:07:33 +0200 blanchet parallelize MeSh file | diff | annotate
Wed, 09 Oct 2013 15:39:34 +0200 blanchet use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected) file | diff | annotate
Wed, 09 Oct 2013 09:47:59 +0200 blanchet optimized built-in const check file | diff | annotate
Fri, 04 Oct 2013 17:00:35 +0200 blanchet more tracing file | diff | annotate
Fri, 04 Oct 2013 16:51:26 +0200 blanchet more thorough spying file | diff | annotate
Fri, 04 Oct 2013 12:59:18 +0200 blanchet removed pointless special case file | diff | annotate
Tue, 01 Oct 2013 15:02:12 +0200 blanchet removed spurious save if nothing needs to bee learned file | diff | annotate
Tue, 24 Sep 2013 12:11:53 +0200 blanchet honor MaSh's zero-overhead policy -- no learning if the tool is disabled file | diff | annotate
Mon, 23 Sep 2013 09:48:06 +0200 blanchet provide a way to override MaSh's port from configuration file file | diff | annotate
Fri, 20 Sep 2013 22:39:30 +0200 blanchet reduce the number of emitted MaSh commands (among others to facilitate debugging) file | diff | annotate
Fri, 20 Sep 2013 22:39:30 +0200 blanchet MaSh tweaks to facilitate debugging file | diff | annotate
Thu, 12 Sep 2013 15:14:54 +0200 blanchet more robust approach to avoid Python byte code -- environment variables get inherited by subprocesses file | diff | annotate
Thu, 12 Sep 2013 11:05:19 +0200 blanchet when pouring in extra features into the goal, only consider facts from the current theory -- the bottom 10 facts of the last import might be completely unrelated file | diff | annotate
Thu, 12 Sep 2013 10:40:53 +0200 blanchet minor fixes file | diff | annotate
Thu, 12 Sep 2013 10:05:10 +0200 blanchet invoke Python with "no bytecode" option to avoid litering Isabelle source directory with ".pyc" files (which can be problematic for a number of reasons) file | diff | annotate
Mon, 26 Aug 2013 12:14:40 +0200 blanchet reverted 6c5e7143e1f6; took a better look at evaluation data this time file | diff | annotate
Mon, 26 Aug 2013 09:07:32 +0200 blanchet tuned fudge factor in light of evaluation file | diff | annotate
Fri, 23 Aug 2013 16:51:53 +0200 blanchet repaired num_extra_feature_facts + tuning file | diff | annotate
Fri, 23 Aug 2013 15:49:27 +0200 blanchet minor MaSh fix file | diff | annotate
Fri, 23 Aug 2013 15:07:32 +0200 blanchet eliminated some needless MaSh features file | diff | annotate
Fri, 23 Aug 2013 14:19:57 +0200 blanchet tuned output file | diff | annotate
Fri, 23 Aug 2013 14:04:08 +0200 blanchet better tracing + honor blocking better file | diff | annotate
Fri, 23 Aug 2013 13:30:25 +0200 blanchet learn new facts on query if there aren't too many of them in MaSh file | diff | annotate
Thu, 22 Aug 2013 23:03:23 +0200 blanchet increase relevance of unknown proximate facts file | diff | annotate
Thu, 22 Aug 2013 23:03:21 +0200 blanchet fixed subtle bug with "take" + thread overlord through file | diff | annotate
Thu, 22 Aug 2013 16:03:13 +0200 blanchet have kill_all also kill MaSh server + be paranoid about reloading after clear_state, to allow for easier experimentation file | diff | annotate
Thu, 22 Aug 2013 12:16:56 +0200 blanchet take chained and proximate facts into consideration when computing MaSh features file | diff | annotate
Thu, 22 Aug 2013 12:12:52 +0200 blanchet pour extra features from proximate facts into goal, in exporter file | diff | annotate
Thu, 22 Aug 2013 08:42:27 +0200 blanchet tuning file | diff | annotate
Wed, 21 Aug 2013 16:21:37 +0200 blanchet improve weight computation for complex terms file | diff | annotate
Wed, 21 Aug 2013 15:34:51 +0200 blanchet improved support for MaSh server file | diff | annotate
Wed, 21 Aug 2013 15:18:06 +0200 blanchet get rid of some silly MaSh features file | diff | annotate
Wed, 21 Aug 2013 14:54:25 +0200 blanchet weight MaSh constants by frequency file | diff | annotate
Wed, 21 Aug 2013 09:25:40 +0200 blanchet only generate feature weights for queries -- they're not used elsewhere file | diff | annotate
Wed, 21 Aug 2013 09:25:40 +0200 blanchet take out dangerous feature, now that all updates are permanent file | diff | annotate
Wed, 21 Aug 2013 09:25:40 +0200 blanchet use new MaSh command-line arguments file | diff | annotate
Wed, 21 Aug 2013 09:25:40 +0200 blanchet shutdown MaSh server file | diff | annotate
Tue, 20 Aug 2013 14:36:22 +0200 blanchet adapted ML code to new version of MaSh tool file | diff | annotate
less more (0) -120 tip
isabelle