# HG changeset patch # User wenzelm # Date 1741027938 -3600 # Node ID cbe937aa5e90c85dc9e0bff20eee647b5dcb7d28 # Parent e4e35ffe1ccd2808c3c03d1c05edee5c6b2cfe7b# Parent dd28f282ddc294cb59b7855f75f6ae7f192f68d6 merged, resolving conflicts in src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML due to clones bb2ea9e80c33 + 62c039ce397c; diff -r dd28f282ddc2 -r cbe937aa5e90 .hgtags --- a/.hgtags Fri Feb 28 13:50:38 2025 +0000 +++ b/.hgtags Mon Mar 03 19:52:18 2025 +0100 @@ -46,3 +46,5 @@ bcb793b951c0d6d2501b2a120ecab37ac7e70d06 Isabelle2025-RC0 ba32209092213c33523db9860a53de75ff5088e4 Isabelle2025-RC1 5888f0bec9718859a47c31da538bdef59c3f38b7 Isabelle2025-RC2 +52290d6ab92d628c7d8a07638b21125e23733e1d Isabelle2025-RC3 +ac7c09c6ff2f6886da114adfa7b1abd690c782ca Isabelle2025-RC4 diff -r dd28f282ddc2 -r cbe937aa5e90 Admin/components/bundled --- a/Admin/components/bundled Fri Feb 28 13:50:38 2025 +0000 +++ b/Admin/components/bundled Mon Mar 03 19:52:18 2025 +0100 @@ -1,2 +1,2 @@ #additional components to be bundled for release -naproche-20250201 +naproche-20250228 diff -r dd28f282ddc2 -r cbe937aa5e90 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Fri Feb 28 13:50:38 2025 +0000 +++ b/Admin/components/components.sha1 Mon Mar 03 19:52:18 2025 +0100 @@ -114,6 +114,7 @@ ae7ee5becb26512f18c609e83b34612918bae5f0 exec_process-1.0.tar.gz a7dffe7ab28c0627ef5957ef521ded2db9022b37 find_facts_web-20250208.tar.gz 2e391c5bfe1dede4c0f9b3b2af6e7227c6e425f4 find_facts_web-20250215.tar.gz +b814ec6f0b0de509bab09fe802c40b1a19b1e578 find_facts_web-20250223.tar.gz 7a4b46752aa60c1ee6c53a2c128dedc8255a4568 flatlaf-0.46-1.tar.gz ed5cbc216389b655dac21a19e770a02a96867b85 flatlaf-0.46.tar.gz d37b38b9a27a6541c644e22eeebe9a339282173d flatlaf-1.0-rc1.tar.gz @@ -365,6 +366,7 @@ f8d093ec54e8df47de0934b329713f59832eb71c naproche-20240519.tar.gz 8212b431b495f2771c3c27bc3ae0418f55cefa88 naproche-20250125.tar.gz da83a3350cf27ca1ab3c86de6b6b60178cfda0db naproche-20250201.tar.gz +434e2a6dc6fe681f7cb7b4e348fd26dbada17e61 naproche-20250228.tar.gz d098dd0873b1720a77dc4e060267f9a6c93f341a naproche-2d99afe5c349.tar.gz 4a4e56fd03b7ba4edd38046f853873a90cf55d1a naproche-4ad61140062f.tar.gz 77252e0b40f89825b9b5935f9f0c4cd5d4e7012a naproche-6d0d76ce2f2a.tar.gz diff -r dd28f282ddc2 -r cbe937aa5e90 Admin/components/main --- a/Admin/components/main Fri Feb 28 13:50:38 2025 +0000 +++ b/Admin/components/main Mon Mar 03 19:52:18 2025 +0100 @@ -8,7 +8,7 @@ elm-0.19.1 easychair-3.5 eptcs-1.7.0 -find_facts_web-20250215 +find_facts_web-20250223 flatlaf-3.5.4-1 foiltex-2.1.4b idea-icons-20210508 diff -r dd28f282ddc2 -r cbe937aa5e90 NEWS --- a/NEWS Fri Feb 28 13:50:38 2025 +0000 +++ b/NEWS Mon Mar 03 19:52:18 2025 +0100 @@ -231,6 +231,14 @@ * Relevant Isabelle options can now be overriden from the Isabelle/VSCode extension settings. +* More robust treatment of startup errors for "isabelle vscode" and the +underlying "isabelle electron". This helps to make it work on recent +Linux distributions, notably Ubuntu 24.04 or 24.10. + +* Proper HTML output on Windows: hyperlinks refer to files in standard +Isabelle path notation as expected. Thus the State panel works again +reliably, after it was broken in Isabelle2022. + *** Document preparation *** @@ -326,7 +334,7 @@ wfp_on_antimono_stronger * Theory "HOL.Transcendental": the real-valued versions of ln, log, -(powr) have been totalised by "ln 0 = x" and "ln (- x) = ln x". Many +(powr) have been totalised by "ln 0 = 0" and "ln (- x) = ln x". Many related theorems are now unconditional, with ln_mult_pos and ln_divide_pos introduced for legacy purposes. @@ -415,7 +423,14 @@ *** System *** * Find_Facts is a full-text search engine as web application based on -Apache Solr (see also https://solr.apache.org). Minimal example: +Apache Solr (see https://solr.apache.org). Example using a bundled +database (if available, +$ISABELLE_HOME/src/Tools/Find_Facts/lib/isabelle.db): + + isabelle find_facts_server -p 8080 -o find_facts_database_name=isabelle + open http://localhost:8080/find_facts#search?q=Hilbert + +Example that builds its own database (called "local" by default): isabelle find_facts_index HOL isabelle find_facts_server -p 8080 diff -r dd28f282ddc2 -r cbe937aa5e90 src/Doc/System/Presentation.thy --- a/src/Doc/System/Presentation.thy Fri Feb 28 13:50:38 2025 +0000 +++ b/src/Doc/System/Presentation.thy Mon Mar 03 19:52:18 2025 +0100 @@ -221,9 +221,9 @@ the search index can be specified via system option @{system_option find_facts_database_name}. A finished search index can be packed for later use as a regular Isabelle component using the - @{tool_def find_facts_index_build} tool: Initializing such a component - causes it to be added to the list of managed components in - @{setting FIND_FACTS_INDEXES}. + @{tool_def find_facts_index_build} tool, with a \<^verbatim>\.db\ file and + \<^verbatim>\etc/settings\ to augment @{setting FIND_FACTS_INDEXES} for use by @{tool + find_facts_server}. \<^medskip> The user interface of the search is available as web application that diff -r dd28f282ddc2 -r cbe937aa5e90 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Fri Feb 28 13:50:38 2025 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Mon Mar 03 19:52:18 2025 +0100 @@ -146,7 +146,7 @@ generate_isabelle_info = false, good_slices = (* FUDGE *) - K [((4, false, false, 60, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))], + K [((2, false, false, 60, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))], good_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), good_max_new_mono_instances = default_max_new_mono_instances} @@ -214,7 +214,7 @@ in (* FUDGE *) [((1000 (* infinity *), false, false, 512, meshN), (format, type_enc, lam_trans, false, extra_options)), - ((2, true, false, 128, mashN), (format, type_enc, combsN, false, extra_options)), + ((1, true, false, 128, mashN), (format, type_enc, combsN, false, extra_options)), ((1000 (* infinity *), false, false, 1024, meshN), (format, type_enc, lam_trans, false, extra_options)), ((1000 (* infinity *), false, false, 64, mepoN), (format, type_enc, lam_trans, false, extra_options)), ((1000 (* infinity *), false, false, 724, meshN), (TF0, "poly_guards??", lam_trans, false, extra_options)), @@ -226,26 +226,26 @@ let val extra_options = "--auto-schedule" val good_slices = - [(((4, false, false, 128, meshN), (TX0_MINUS, "mono_native_fool", liftingN, false, extra_options))), - (((4, false, false, 1024, meshN), (TH0, "mono_native_higher", keep_lamsN, false, extra_options))), - (((4, false, false, 128, meshN), (TH0_MINUS, "mono_native_higher", keep_lamsN, false, extra_options))), - (((4, false, false, 2048, meshN), (TF0, "mono_native", combsN, false, extra_options))), - (((4, false, false, 512, meshN), (TF0, "mono_native", liftingN, false, extra_options))), - (((4, false, false, 1024, meshN), (TX0_MINUS, "mono_native_fool", liftingN, false, extra_options))), - (((4, false, false, 64, meshN), (TH0, "mono_native_higher", keep_lamsN, false, extra_options))), - (((4, false, false, 512, meshN), (TH0_MINUS, "mono_native_higher", keep_lamsN, false, extra_options))), - (((4, false, false, 32, meshN), (TF0, "mono_native", liftingN, false, extra_options))), - (((4, false, false, 2048, meshN), (TH0, "mono_native_higher", keep_lamsN, false, extra_options))), - (((4, false, false, 256, meshN), (TH0, "mono_native_higher", keep_lamsN, false, extra_options))), - (((4, false, false, 512, meshN), (TF0, "mono_native", combsN, false, extra_options))), - (((4, false, false, 1024, meshN), (TF0, "mono_native", liftingN, false, extra_options))), - (((4, false, false, 16, meshN), (TH0, "mono_native_higher", keep_lamsN, false, extra_options))), - (((4, false, false, 512, meshN), (TX0_MINUS, "mono_native_fool", liftingN, false, extra_options))), - (((4, false, false, 64, meshN), (TF0, "mono_native", liftingN, false, extra_options))), - (((4, false, false, 128, meshN), (TF0, "mono_native", combsN, false, extra_options))), - (((4, false, false, 2048, meshN), (TH0_MINUS, "mono_native_higher", keep_lamsN, false, extra_options))), - (((4, false, false, 128, meshN), (TX0_MINUS, "mono_native_fool", combsN, false, extra_options))), - (((4, false, false, 2048, meshN), (TX0_MINUS, "mono_native_fool", liftingN, false, extra_options)))] + [(((2, false, false, 128, meshN), (TX0_MINUS, "mono_native_fool", liftingN, false, extra_options))), + (((2, false, false, 1024, meshN), (TH0, "mono_native_higher", keep_lamsN, false, extra_options))), + (((2, false, false, 128, meshN), (TH0_MINUS, "mono_native_higher", keep_lamsN, false, extra_options))), + (((2, false, false, 2048, meshN), (TF0, "mono_native", combsN, false, extra_options))), + (((2, false, false, 512, meshN), (TF0, "mono_native", liftingN, false, extra_options))), + (((2, false, false, 1024, meshN), (TX0_MINUS, "mono_native_fool", liftingN, false, extra_options))), + (((2, false, false, 64, meshN), (TH0, "mono_native_higher", keep_lamsN, false, extra_options))), + (((2, false, false, 512, meshN), (TH0_MINUS, "mono_native_higher", keep_lamsN, false, extra_options))), + (((2, false, false, 32, meshN), (TF0, "mono_native", liftingN, false, extra_options))), + (((2, false, false, 2048, meshN), (TH0, "mono_native_higher", keep_lamsN, false, extra_options))), + (((2, false, false, 256, meshN), (TH0, "mono_native_higher", keep_lamsN, false, extra_options))), + (((2, false, false, 512, meshN), (TF0, "mono_native", combsN, false, extra_options))), + (((2, false, false, 1024, meshN), (TF0, "mono_native", liftingN, false, extra_options))), + (((2, false, false, 16, meshN), (TH0, "mono_native_higher", keep_lamsN, false, extra_options))), + (((2, false, false, 512, meshN), (TX0_MINUS, "mono_native_fool", liftingN, false, extra_options))), + (((2, false, false, 64, meshN), (TF0, "mono_native", liftingN, false, extra_options))), + (((2, false, false, 128, meshN), (TF0, "mono_native", combsN, false, extra_options))), + (((2, false, false, 2048, meshN), (TH0_MINUS, "mono_native_higher", keep_lamsN, false, extra_options))), + (((2, false, false, 128, meshN), (TX0_MINUS, "mono_native_fool", combsN, false, extra_options))), + (((2, false, false, 2048, meshN), (TX0_MINUS, "mono_native_fool", liftingN, false, extra_options)))] in make_e_config 128 good_slices end @@ -277,11 +277,11 @@ generate_isabelle_info = false, good_slices = (* FUDGE *) - K [((4, false, false, 32, meshN), (TF0, "mono_native", liftingN, false, "")), - ((4, false, false, 512, meshN), (TX0, "mono_native", liftingN, false, "")), - ((4, false, false, 128, mashN), (TF0, "mono_native", combsN, false, "")), - ((4, false, false, 1024, meshN), (TF0, "mono_native", liftingN, false, "")), - ((4, false, true, 256, mepoN), (TF0, "mono_native", combsN, false, ""))], + K [((2, false, false, 32, meshN), (TF0, "mono_native", liftingN, false, "")), + ((2, false, false, 512, meshN), (TX0, "mono_native", liftingN, false, "")), + ((2, false, false, 128, mashN), (TF0, "mono_native", combsN, false, "")), + ((2, false, false, 1024, meshN), (TF0, "mono_native", liftingN, false, "")), + ((2, false, true, 256, mepoN), (TF0, "mono_native", combsN, false, ""))], good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = default_max_new_mono_instances} @@ -307,7 +307,7 @@ generate_isabelle_info = false, good_slices = (* FUDGE *) - K [((4, false, false, 40, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))], + K [((2, false, false, 40, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))], good_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), good_max_new_mono_instances = default_max_new_mono_instances} @@ -389,14 +389,14 @@ generate_isabelle_info = true, good_slices = (* FUDGE *) - K [((4, false, false, 150, meshN), (DFG Monomorphic, "mono_native", combsN, true, "")), - ((4, false, false, 500, meshN), (DFG Monomorphic, "mono_native", liftingN, true, spass_H2SOS)), - ((4, false, false, 50, meshN), (DFG Monomorphic, "mono_native", liftingN, true, spass_H2LR0LT0)), - ((4, false, false, 250, meshN), (DFG Monomorphic, "mono_native", combsN, true, spass_H2NuVS0)), - ((4, false, false, 1000, mepoN), (DFG Monomorphic, "mono_native", liftingN, true, spass_H1SOS)), - ((4, false, true, 150, meshN), (DFG Monomorphic, "poly_guards??", liftingN, false, spass_H2NuVS0Red2)), - ((4, false, false, 300, meshN), (DFG Monomorphic, "mono_native", combsN, true, spass_H2SOS)), - ((4, false, false, 100, meshN), (DFG Monomorphic, "mono_native", combs_and_liftingN, true, spass_H2))], + K [((2, false, false, 150, meshN), (DFG Monomorphic, "mono_native", combsN, true, "")), + ((2, false, false, 500, meshN), (DFG Monomorphic, "mono_native", liftingN, true, spass_H2SOS)), + ((2, false, false, 50, meshN), (DFG Monomorphic, "mono_native", liftingN, true, spass_H2LR0LT0)), + ((2, false, false, 250, meshN), (DFG Monomorphic, "mono_native", combsN, true, spass_H2NuVS0)), + ((2, false, false, 1000, mepoN), (DFG Monomorphic, "mono_native", liftingN, true, spass_H1SOS)), + ((2, false, true, 150, meshN), (DFG Monomorphic, "poly_guards??", liftingN, false, spass_H2NuVS0Red2)), + ((2, false, false, 300, meshN), (DFG Monomorphic, "mono_native", combsN, true, spass_H2SOS)), + ((2, false, false, 100, meshN), (DFG Monomorphic, "mono_native", combs_and_liftingN, true, spass_H2))], good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = default_max_new_mono_instances} @@ -514,21 +514,21 @@ prem_role = Hypothesis, generate_isabelle_info = true, good_slices = - K [((2, false, false, 512, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --max-inferences=1 --ho-unif-max-depth=1 --ho-max-elims=0 --ho-max-app-projections=0 --ho-max-rigid-imitations=1 --ho-max-identifications=0 --boolean-reasoning=bool-hoist --bool-hoist-simpl=true --bool-select=LI --recognize-injectivity=true --ext-rules=ext-family --ext-rules-max-depth=1 --ho-choice-inst=true --ho-prim-enum=none --ho-elim-leibniz=0 --interpret-bool-funs=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --ho-unif-level=pragmatic-framework --select=bb+e-selection2 --post-cnf-lambda-lifting=true -q \"4|prefer-sos|pnrefined(2,1,1,1,2,2,2)\" -q \"6|prefer-processed|conjecture-relative-struct(1.5,3.5,2,3)\" -q \"1|const|fifo\" -q \"4|prefer-ground|orient-lmax(2,1,2,1,1)\" -q \"4|defer-sos|conjecture-relative-struct(1,5,2,3)\" --avatar=off --recognize-injectivity=true --ho-neg-ext=true --e-timeout=2 --ho-pattern-decider=true --ho-fixpoint-decider=true --e-max-derived=50 --ignore-orphans=true --e-auto=true --presaturate=true --e-call-point=0.1")), (* sh5_sh1.sh *) - ((2, false, false, 512, mepoN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic -nc --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=none --avatar=off --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars --max-inferences=4 --ho-max-app-projections=1 --ho-max-elims=0 --ho-max-rigid-imitations=2 --ho-max-identifications=0 --ho-unif-max-depth=3 -q \"6|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"6|const|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-easy-ho|conjecture-relative-var(1.01,s,f)\" --select=e-selection7 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=7 --sine=50 --sine-tolerance=1 --sine-depth-max=2 --sine-depth-min=1 --e-max-derived=64 --sine-ignore-k-most-common-syms=2 --sine-trim-implications=true --e-encode-lambdas=lift --scan-clause-ac=false --lambdasup=0 --kbo-weight-fun=lambda-def-invfreqrank --demod-in-var-args=true --bool-demod=true --lambda-demod=true --e-call-point=0.1")), (* sh10_c_ic.sh *) - ((2, false, false, 1024, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=none --avatar=off --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars --max-inferences=2 --ho-unif-max-depth=1 -q \"6|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"6|const|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-easy-ho|conjecture-relative-var(1.01,s,f)\" --select=e-selection16 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-auto=true --sine=50 --sine-tolerance=1.0 --sine-depth-max=3 --sine-depth-min=1 --sine-trim-implications=true --ho-unif-level=pragmatic-framework --e-encode-lambdas=lift --scan-clause-ac=false --kbo-weight-fun=lambda-def-invfreqrank --e-call-point=0.1")), (* sh8_shallow_sine.sh *) - ((2, false, false, 256, mepoN), (format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=off --ho-prim-enum=full --ho-prim-max=1 --avatar=off --recognize-injectivity=true --ho-elim-leibniz=4 --ho-unif-level=full-framework --no-max-vars -q \"2|prefer-goals|conjecture-relative-e(0.5,1,100,100,100,100,1.5,1.5,1)\" -q \"4|const|conjecture-relative-e(0.1,1,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-e(0.5,1,100,100,100,100,1.5,1.5,1.5)\" -q \"4|prefer-sos|pnrefined(1,1,1,1,2,1.5,2)\" --select=ho-selection5 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=5 --e-call-point=0.25 --e-auto=true --sine=50 --sine-tolerance=2 --sine-depth-max=4 --sine-depth-min=1 --e-max-derived=96 --e-encode-lambdas=lift --scan-clause-ac=false --kbo-weight-fun=arity0 --prec-gen-fun=invfreq_conj")), (* sh10_new_c.s3.sh *) - ((2, false, true, 512, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-comb-complete --boolean-reasoning=simpl-only --ext-rules=off --kbo-weight-fun=lambda-def-sqarity --ho-prim-enum=none --tptp-def-as-rewrite -q \"4|prefer-sos|orient-lmax(2,1,2,1,1)\" -q \"4|defer-sos|conjecture-relative-var(1,s,f)\" -q \"3|const|default\" -q \"1|prefer-processed|fifo\" --ho-elim-leibniz=1 --select=NoSelection --solve-formulas=true --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=8 --sine=60 --sine-tolerance=2 --sine-depth-max=5 --sine-depth-min=1 --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-auto=true --e-max-derived=50 --e-encode-lambdas=lift --scan-clause-ac=false --presaturate=true --comb-b-penalty=3 --comb-c-penalty=3 --comb-k-penalty=1 --comb-s-penalty=5 --subvarsup=false --e-call-point=0.15")), (* sh8_b.comb.sh (modified) *) - ((2, false, false, 1024, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --boolean-reasoning=simpl-only --ho-unif-max-depth=0 --ho-prim-enum=none -q \"2|prefer-ho-steps|conjecture-relative-e(0.1,0.5,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"2|prefer-ground|default\" -q \"2|prefer-empty-trail|conjecture-relative-e(0.1,0.5,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-processed|fifo\" --select=bb+e-selection7 --ho-pattern-decider=false --ho-fixpoint-decider=true --ho-solid-decider=false --sine=150 --sine-tolerance=2 --sine-depth-max=3 --sine-depth-min=1 --prec-gen-fun=invfreqhack --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=2 --fluid-log-hoist=false --tptp-def-as-rewrite --rewrite-before-cnf=true --ho-prim-enum=eq --ho-prim-enum-add-var=true --ho-prim-max=1 --ho-prim-enum-early-bird=true --avatar=eager --split-only-ground=true")), (* sh5_add_var_l_av.sh *) - ((2, false, false, 256, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --max-inferences=4 --ho-max-app-projections=1 --ho-max-elims=0 --ho-max-rigid-imitations=2 --ho-max-identifications=0 --ho-unif-max-depth=2 --max-inferences=3 --boolean-reasoning=bool-hoist --bool-select=LO --ext-rules=off --kbo-weight-fun=lambda-def-invfreqrank --ho-prim-enum=none --ho-unif-level=pragmatic-framework -q \"1|prefer-sos|conjecture-relative-var(1.01,s,f)\" -q \"4|const|conjecture-relative-var(1.05,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1.02,l,f)\" -q \"4|prefer-sos|pnrefined(3,2,3,2,2,1.5,2)\" --ho-elim-leibniz=1 --ho-fixpoint-decider=true --ho-pattern-decider=true --ho-solid-decider=true --select=e-selection2 --solve-formulas=true --lambdasup=0 --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-max-derived=48 --e-encode-lambdas=lift --presaturate=true --prec-gen-fun=invfreq --e-call-point=0.2 --e-auto=true --sine-trim-implications=true")), (* sh10_e_lift.sh *) - ((2, false, false, 512, mepoN), (format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --mode=ho-pragmatic --max-inferences=4 --ho-max-app-projections=1 --ho-max-elims=0 --ho-max-rigid-imitations=1 --ho-max-identifications=0 --ho-unif-max-depth=2 --boolean-reasoning=simpl-only --ext-rules=off --kbo-weight-fun=lambda-def-const --ho-prim-enum=neg --ho-prim-enum-early-bird=true --tptp-def-as-rewrite --rewrite-before-cnf=true --ho-unif-level=pragmatic-framework --ho-unif-max-depth=1 --sine=50 --sine-tolerance=1.0 --sine-depth-max=3 --sine-depth-min=1 --sine-trim-implications=true -q \"4|prefer-sos|orient-lmax(2,1,2,1,1)\" -q \"4|defer-sos|conjecture-relative-var(1,s,f)\" -q \"3|const|default\" -q \"1|prefer-processed|fifo\" --ho-elim-leibniz=1 --ho-fixpoint-decider=true --ho-pattern-decider=true --ho-solid-decider=false --select=e-selection10 --solve-formulas=true --sup-at-vars=false --sup-at-var-headed=false --sup-from-var-headed=true --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=4 --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=2 --e-auto=true --e-max-derived=32 --e-encode-lambdas=lift --scan-clause-ac=false --presaturate=true --e-call-point=0.16")), (* sh5_shallow_sine.sh *) - ((2, false, false, 512, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=bool-hoist --ext-rules=off --recognize-injectivity=true --ho-unif-level=full-framework -q \"4|prefer-goals|pnrefined(1,1,1,2,2,2,0.5)\" -q \"1|prefer-fo|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-ho-steps|conjecture-relative-var(1.01,s,f)\" -q \"1|prefer-processed|fifo\" --select=bb+ho-selection --scan-clause-ac=false --kbo-weight-fun=invfreqrank --fluidsup=true --boolean-reasoning=bool-hoist --fluid-log-hoist=true --fluid-hoist=true --ite-axioms=true --lazy-cnf=true --ho-solid-decider=true --ho-fixpoint-decider=true --bool-select=\"sel1(pos_ctx)\" --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=2 --e-auto=true --e-call-point=0.35 --avatar=off --e-max-derived=50")), (* sh5_e_short1.sh *) - ((2, false, false, 1024, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --boolean-reasoning=simpl-only --select=e-selection12 --prec-gen-fun=invfreq_conj --ord=lambda_kbo --ho-unif-level=full-framework --ho-pattern-decider=true --ho-solid-decider=false --ho-fixpoint-decider=true --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=1 --sine=100 --sine-depth-min=1 --sine-depth-max=5 --sine-tolerance=1.5 -q \"1|prefer-sos|default\" -q \"8|prefer-processed|conjecture-relative-var(1,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-lambdas|explore\" -q \"1|prefer-non-goals|explore\" -q \"1|prefer-processed|conjecture-relative-var(1,s,f)\" --kbo-weight-fun=arity0")), (* sh5_32.sh *) - ((2, false, false, 256, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --boolean-reasoning=simpl-only --ho-unif-max-depth=2 --ho-max-app-projections=0 --ho-max-rigid-imitations=1 --ho-max-elims=0 --ho-max-identifications=1 --max-inferences=3 --ext-rules=off --recognize-injectivity=true --ho-prim-enum=none --ho-choice-inst=true -q \"3|prefer-fo|conjecture-relative-var(1.02,l,f)\" -q \"3|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"2|prefer-ground|orient-lmax(2,1,2,1,1)\" -q \"1|prefer-processed|fifo\" --select=MaxGoalNS --sine=60 --sine-tolerance=1.5 --sine-depth-max=3 --sine-depth-min=1 --prec-gen-fun=invfreqhack --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=3 --kbo-weight-fun-from-precedence=true --kbo-weight-fun-from-precedence-rank=5 --trigger-bool-inst=1 --avatar=lazy --tptp-def-as-rewrite --rewrite-before-cnf=true --sup-from-var-headed=false --sup-at-vars=false")), (* sh5_sh4.sh *) - ((2, false, false, 512, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "--tptp-def-as-rewrite --rewrite-before-cnf=true --mode=lambda-free-intensional --check-lambda-free=false --boolean-reasoning=simpl-only --post-cnf-lambda-lifting=true --ext-rules=off --ho-prim-enum=none --recognize-injectivity=true --no-max-vars --select=e-selection8 --prec-gen-fun=invfreq --kbo-weight-fun=invfreqrank --kbo-const-weight=2 --ord=lambdafree_kbo --ignore-orphans=true -q \"1|prefer-sos|conjecture-relative-struct(1.5,3.5,2,3)\" -q \"1|const|conj_pref_weight(0.5,100,0.2,0.2,4)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-e(0.3,0.25,100,100,100,100,1.5,1.5,1)\" -q \"1|prefer-sos|pnrefined(3,2,3,2,2,1.5,2)\" --lazy-cnf=true --lazy-cnf-renaming-threshold=2")), (* sh5_lifting2.sh *) - ((2, false, false, 512, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --rewrite-before-cnf=true --tptp-rewrite-formulas-only=true --mode=ho-pragmatic --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=neg --ho-prim-max=1 --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars -q \"1|prefer-sos|conjecture-relative-var(1.02,l,f)\" -q \"4|const|conjecture-relative-var(1,s,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-sos|pnrefined(2,1,1,1,2,2,2)\" --select=e-selection7 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=2 --e-auto=true --sine=50 --sine-tolerance=10 --sine-depth-max=5 --sine-depth-min=1 --e-max-derived=64 --e-encode-lambdas=lift --scan-clause-ac=false --prec-gen-fun=invfreq_conj --ord=lambda_kbo --solid-subsumption=true --ignore-orphans=true --e-call-point=0.2")), (* sh5_noforms.sh *) - ((2, false, false, 1024, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --max-inferences=4 --ho-unif-max-depth=3 --ho-max-elims=0 --ho-max-app-projections=1 --ho-max-identifications=0 --ho-max-rigid-imitations=2 --ho-unif-level=pragmatic-framework --boolean-reasoning=simpl-only --kbo-weight-fun=freqrank --ext-rules=ext-family --ext-rules-max-depth=2 --ho-prim-enum=eq --ho-prim-max=2 --interpret-bool-funs=false -q \"2|prefer-goals|default\" -q \"8|prefer-sos|conjecture-relative-var(1,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-lambdas|explore\" -q \"1|prefer-non-goals|explore\" -q \"1|prefer-processed|conjecture-relative-var(1,s,f)\" --recognize-injectivity=true --ho-selection-restriction=none --select=ho-selection2 --solve-formulas=true")), (* sh8_old_zip1.sh *) - ((2, false, false, 256, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --boolean-reasoning=simpl-only --tptp-def-as-rewrite --rewrite-before-cnf=true --kbo-weight-fun=freqrank -q \"1|prefer-sos|default\" -q \"1|prefer-goals|conjecture-relative-var(1.03,s,f)\" -q \"1|prefer-non-goals|default\" -q \"5|const|conjecture-relative-var(1.01,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|const|conjecture-relative-var(1.05,l,f)\" -q \"1|defer-sos|conjecture-relative-var(1.1,s,f)\" --select=e-selection9 --recognize-injectivity=true --ho-choice-inst=false --ho-selection-restriction=none --sine=50 --sine-tolerance=3 --sine-depth-max=3 --sine-depth-min=1 --eq-encode=true --avatar=eager --sine-trim-implications=true"))], (* sh5_sh.eqenc.sh *) + K [((1, false, false, 512, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --max-inferences=1 --ho-unif-max-depth=1 --ho-max-elims=0 --ho-max-app-projections=0 --ho-max-rigid-imitations=1 --ho-max-identifications=0 --boolean-reasoning=bool-hoist --bool-hoist-simpl=true --bool-select=LI --recognize-injectivity=true --ext-rules=ext-family --ext-rules-max-depth=1 --ho-choice-inst=true --ho-prim-enum=none --ho-elim-leibniz=0 --interpret-bool-funs=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --ho-unif-level=pragmatic-framework --select=bb+e-selection2 --post-cnf-lambda-lifting=true -q \"4|prefer-sos|pnrefined(2,1,1,1,2,2,2)\" -q \"6|prefer-processed|conjecture-relative-struct(1.5,3.5,2,3)\" -q \"1|const|fifo\" -q \"4|prefer-ground|orient-lmax(2,1,2,1,1)\" -q \"4|defer-sos|conjecture-relative-struct(1,5,2,3)\" --avatar=off --recognize-injectivity=true --ho-neg-ext=true --e-timeout=2 --ho-pattern-decider=true --ho-fixpoint-decider=true --e-max-derived=50 --ignore-orphans=true --e-auto=true --presaturate=true --e-call-point=0.1")), (* sh5_sh1.sh *) + ((1, false, false, 512, mepoN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic -nc --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=none --avatar=off --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars --max-inferences=4 --ho-max-app-projections=1 --ho-max-elims=0 --ho-max-rigid-imitations=2 --ho-max-identifications=0 --ho-unif-max-depth=3 -q \"6|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"6|const|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-easy-ho|conjecture-relative-var(1.01,s,f)\" --select=e-selection7 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=7 --sine=50 --sine-tolerance=1 --sine-depth-max=2 --sine-depth-min=1 --e-max-derived=64 --sine-ignore-k-most-common-syms=2 --sine-trim-implications=true --e-encode-lambdas=lift --scan-clause-ac=false --lambdasup=0 --kbo-weight-fun=lambda-def-invfreqrank --demod-in-var-args=true --bool-demod=true --lambda-demod=true --e-call-point=0.1")), (* sh10_c_ic.sh *) + ((1, false, false, 1024, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=none --avatar=off --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars --max-inferences=2 --ho-unif-max-depth=1 -q \"6|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"6|const|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-easy-ho|conjecture-relative-var(1.01,s,f)\" --select=e-selection16 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-auto=true --sine=50 --sine-tolerance=1.0 --sine-depth-max=3 --sine-depth-min=1 --sine-trim-implications=true --ho-unif-level=pragmatic-framework --e-encode-lambdas=lift --scan-clause-ac=false --kbo-weight-fun=lambda-def-invfreqrank --e-call-point=0.1")), (* sh8_shallow_sine.sh *) + ((1, false, false, 256, mepoN), (format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=off --ho-prim-enum=full --ho-prim-max=1 --avatar=off --recognize-injectivity=true --ho-elim-leibniz=4 --ho-unif-level=full-framework --no-max-vars -q \"2|prefer-goals|conjecture-relative-e(0.5,1,100,100,100,100,1.5,1.5,1)\" -q \"4|const|conjecture-relative-e(0.1,1,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-e(0.5,1,100,100,100,100,1.5,1.5,1.5)\" -q \"4|prefer-sos|pnrefined(1,1,1,1,2,1.5,2)\" --select=ho-selection5 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=5 --e-call-point=0.25 --e-auto=true --sine=50 --sine-tolerance=2 --sine-depth-max=4 --sine-depth-min=1 --e-max-derived=96 --e-encode-lambdas=lift --scan-clause-ac=false --kbo-weight-fun=arity0 --prec-gen-fun=invfreq_conj")), (* sh10_new_c.s3.sh *) + ((1, false, true, 512, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-comb-complete --boolean-reasoning=simpl-only --ext-rules=off --kbo-weight-fun=lambda-def-sqarity --ho-prim-enum=none --tptp-def-as-rewrite -q \"4|prefer-sos|orient-lmax(2,1,2,1,1)\" -q \"4|defer-sos|conjecture-relative-var(1,s,f)\" -q \"3|const|default\" -q \"1|prefer-processed|fifo\" --ho-elim-leibniz=1 --select=NoSelection --solve-formulas=true --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=8 --sine=60 --sine-tolerance=2 --sine-depth-max=5 --sine-depth-min=1 --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-auto=true --e-max-derived=50 --e-encode-lambdas=lift --scan-clause-ac=false --presaturate=true --comb-b-penalty=3 --comb-c-penalty=3 --comb-k-penalty=1 --comb-s-penalty=5 --subvarsup=false --e-call-point=0.15")), (* sh8_b.comb.sh (modified) *) + ((1, false, false, 1024, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --boolean-reasoning=simpl-only --ho-unif-max-depth=0 --ho-prim-enum=none -q \"2|prefer-ho-steps|conjecture-relative-e(0.1,0.5,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"2|prefer-ground|default\" -q \"2|prefer-empty-trail|conjecture-relative-e(0.1,0.5,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-processed|fifo\" --select=bb+e-selection7 --ho-pattern-decider=false --ho-fixpoint-decider=true --ho-solid-decider=false --sine=150 --sine-tolerance=2 --sine-depth-max=3 --sine-depth-min=1 --prec-gen-fun=invfreqhack --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=2 --fluid-log-hoist=false --tptp-def-as-rewrite --rewrite-before-cnf=true --ho-prim-enum=eq --ho-prim-enum-add-var=true --ho-prim-max=1 --ho-prim-enum-early-bird=true --avatar=eager --split-only-ground=true")), (* sh5_add_var_l_av.sh *) + ((1, false, false, 256, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --max-inferences=4 --ho-max-app-projections=1 --ho-max-elims=0 --ho-max-rigid-imitations=2 --ho-max-identifications=0 --ho-unif-max-depth=2 --max-inferences=3 --boolean-reasoning=bool-hoist --bool-select=LO --ext-rules=off --kbo-weight-fun=lambda-def-invfreqrank --ho-prim-enum=none --ho-unif-level=pragmatic-framework -q \"1|prefer-sos|conjecture-relative-var(1.01,s,f)\" -q \"4|const|conjecture-relative-var(1.05,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1.02,l,f)\" -q \"4|prefer-sos|pnrefined(3,2,3,2,2,1.5,2)\" --ho-elim-leibniz=1 --ho-fixpoint-decider=true --ho-pattern-decider=true --ho-solid-decider=true --select=e-selection2 --solve-formulas=true --lambdasup=0 --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-max-derived=48 --e-encode-lambdas=lift --presaturate=true --prec-gen-fun=invfreq --e-call-point=0.2 --e-auto=true --sine-trim-implications=true")), (* sh10_e_lift.sh *) + ((1, false, false, 512, mepoN), (format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --mode=ho-pragmatic --max-inferences=4 --ho-max-app-projections=1 --ho-max-elims=0 --ho-max-rigid-imitations=1 --ho-max-identifications=0 --ho-unif-max-depth=2 --boolean-reasoning=simpl-only --ext-rules=off --kbo-weight-fun=lambda-def-const --ho-prim-enum=neg --ho-prim-enum-early-bird=true --tptp-def-as-rewrite --rewrite-before-cnf=true --ho-unif-level=pragmatic-framework --ho-unif-max-depth=1 --sine=50 --sine-tolerance=1.0 --sine-depth-max=3 --sine-depth-min=1 --sine-trim-implications=true -q \"4|prefer-sos|orient-lmax(2,1,2,1,1)\" -q \"4|defer-sos|conjecture-relative-var(1,s,f)\" -q \"3|const|default\" -q \"1|prefer-processed|fifo\" --ho-elim-leibniz=1 --ho-fixpoint-decider=true --ho-pattern-decider=true --ho-solid-decider=false --select=e-selection10 --solve-formulas=true --sup-at-vars=false --sup-at-var-headed=false --sup-from-var-headed=true --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=4 --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=2 --e-auto=true --e-max-derived=32 --e-encode-lambdas=lift --scan-clause-ac=false --presaturate=true --e-call-point=0.16")), (* sh5_shallow_sine.sh *) + ((1, false, false, 512, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=bool-hoist --ext-rules=off --recognize-injectivity=true --ho-unif-level=full-framework -q \"4|prefer-goals|pnrefined(1,1,1,2,2,2,0.5)\" -q \"1|prefer-fo|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-ho-steps|conjecture-relative-var(1.01,s,f)\" -q \"1|prefer-processed|fifo\" --select=bb+ho-selection --scan-clause-ac=false --kbo-weight-fun=invfreqrank --fluidsup=true --boolean-reasoning=bool-hoist --fluid-log-hoist=true --fluid-hoist=true --ite-axioms=true --lazy-cnf=true --ho-solid-decider=true --ho-fixpoint-decider=true --bool-select=\"sel1(pos_ctx)\" --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=2 --e-auto=true --e-call-point=0.35 --avatar=off --e-max-derived=50")), (* sh5_e_short1.sh *) + ((1, false, false, 1024, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --boolean-reasoning=simpl-only --select=e-selection12 --prec-gen-fun=invfreq_conj --ord=lambda_kbo --ho-unif-level=full-framework --ho-pattern-decider=true --ho-solid-decider=false --ho-fixpoint-decider=true --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=1 --sine=100 --sine-depth-min=1 --sine-depth-max=5 --sine-tolerance=1.5 -q \"1|prefer-sos|default\" -q \"8|prefer-processed|conjecture-relative-var(1,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-lambdas|explore\" -q \"1|prefer-non-goals|explore\" -q \"1|prefer-processed|conjecture-relative-var(1,s,f)\" --kbo-weight-fun=arity0")), (* sh5_32.sh *) + ((1, false, false, 256, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --boolean-reasoning=simpl-only --ho-unif-max-depth=2 --ho-max-app-projections=0 --ho-max-rigid-imitations=1 --ho-max-elims=0 --ho-max-identifications=1 --max-inferences=3 --ext-rules=off --recognize-injectivity=true --ho-prim-enum=none --ho-choice-inst=true -q \"3|prefer-fo|conjecture-relative-var(1.02,l,f)\" -q \"3|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"2|prefer-ground|orient-lmax(2,1,2,1,1)\" -q \"1|prefer-processed|fifo\" --select=MaxGoalNS --sine=60 --sine-tolerance=1.5 --sine-depth-max=3 --sine-depth-min=1 --prec-gen-fun=invfreqhack --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=3 --kbo-weight-fun-from-precedence=true --kbo-weight-fun-from-precedence-rank=5 --trigger-bool-inst=1 --avatar=lazy --tptp-def-as-rewrite --rewrite-before-cnf=true --sup-from-var-headed=false --sup-at-vars=false")), (* sh5_sh4.sh *) + ((1, false, false, 512, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "--tptp-def-as-rewrite --rewrite-before-cnf=true --mode=lambda-free-intensional --check-lambda-free=false --boolean-reasoning=simpl-only --post-cnf-lambda-lifting=true --ext-rules=off --ho-prim-enum=none --recognize-injectivity=true --no-max-vars --select=e-selection8 --prec-gen-fun=invfreq --kbo-weight-fun=invfreqrank --kbo-const-weight=2 --ord=lambdafree_kbo --ignore-orphans=true -q \"1|prefer-sos|conjecture-relative-struct(1.5,3.5,2,3)\" -q \"1|const|conj_pref_weight(0.5,100,0.2,0.2,4)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-e(0.3,0.25,100,100,100,100,1.5,1.5,1)\" -q \"1|prefer-sos|pnrefined(3,2,3,2,2,1.5,2)\" --lazy-cnf=true --lazy-cnf-renaming-threshold=2")), (* sh5_lifting2.sh *) + ((1, false, false, 512, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --rewrite-before-cnf=true --tptp-rewrite-formulas-only=true --mode=ho-pragmatic --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=neg --ho-prim-max=1 --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars -q \"1|prefer-sos|conjecture-relative-var(1.02,l,f)\" -q \"4|const|conjecture-relative-var(1,s,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-sos|pnrefined(2,1,1,1,2,2,2)\" --select=e-selection7 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=2 --e-auto=true --sine=50 --sine-tolerance=10 --sine-depth-max=5 --sine-depth-min=1 --e-max-derived=64 --e-encode-lambdas=lift --scan-clause-ac=false --prec-gen-fun=invfreq_conj --ord=lambda_kbo --solid-subsumption=true --ignore-orphans=true --e-call-point=0.2")), (* sh5_noforms.sh *) + ((1, false, false, 1024, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --max-inferences=4 --ho-unif-max-depth=3 --ho-max-elims=0 --ho-max-app-projections=1 --ho-max-identifications=0 --ho-max-rigid-imitations=2 --ho-unif-level=pragmatic-framework --boolean-reasoning=simpl-only --kbo-weight-fun=freqrank --ext-rules=ext-family --ext-rules-max-depth=2 --ho-prim-enum=eq --ho-prim-max=2 --interpret-bool-funs=false -q \"2|prefer-goals|default\" -q \"8|prefer-sos|conjecture-relative-var(1,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-lambdas|explore\" -q \"1|prefer-non-goals|explore\" -q \"1|prefer-processed|conjecture-relative-var(1,s,f)\" --recognize-injectivity=true --ho-selection-restriction=none --select=ho-selection2 --solve-formulas=true")), (* sh8_old_zip1.sh *) + ((1, false, false, 256, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --boolean-reasoning=simpl-only --tptp-def-as-rewrite --rewrite-before-cnf=true --kbo-weight-fun=freqrank -q \"1|prefer-sos|default\" -q \"1|prefer-goals|conjecture-relative-var(1.03,s,f)\" -q \"1|prefer-non-goals|default\" -q \"5|const|conjecture-relative-var(1.01,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|const|conjecture-relative-var(1.05,l,f)\" -q \"1|defer-sos|conjecture-relative-var(1.1,s,f)\" --select=e-selection9 --recognize-injectivity=true --ho-choice-inst=false --ho-selection-restriction=none --sine=50 --sine-tolerance=3 --sine-depth-max=3 --sine-depth-min=1 --eq-encode=true --avatar=eager --sine-trim-implications=true"))], (* sh5_sh.eqenc.sh *) good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = default_max_new_mono_instances} end @@ -646,7 +646,7 @@ prem_role = prem_role, generate_isabelle_info = false, good_slices = - K [((4, false, false, 256, "mepo"), (format, type_enc, + K [((2, false, false, 256, "mepo"), (format, type_enc, if is_format_higher_order format then keep_lamsN else combsN, uncurried_aliases, ""))], good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = default_max_new_mono_instances} diff -r dd28f282ddc2 -r cbe937aa5e90 src/Pure/Admin/build_release.scala --- a/src/Pure/Admin/build_release.scala Fri Feb 28 13:50:38 2025 +0000 +++ b/src/Pure/Admin/build_release.scala Mon Mar 03 19:52:18 2025 +0100 @@ -6,6 +6,8 @@ package isabelle +import isabelle.find_facts.Find_Facts + object Build_Release { /** release context **/ @@ -496,9 +498,9 @@ val database_dir = other_isabelle.expand_path( Path.explode("$FIND_FACTS_HOME_USER/solr") + Path.basic(database_name)) - val database_target_dir = + val database_target = other_isabelle.expand_path( - Path.explode("$FIND_FACTS_HOME/lib/find_facts-" + database_name)) + Path.explode("$FIND_FACTS_HOME/lib") + Path.basic(database_name).db) val sessions = other_isabelle.bash("bin/isabelle sessions -a " + opt_dirs).check.out_lines @@ -506,8 +508,7 @@ "bin/isabelle find_facts_index -o find_facts_database_name=" + Bash.string(database_name) + " -n -N " + opt_dirs + Bash.strings(sessions), echo = true).check - Isabelle_System.make_directory(database_target_dir) - Isabelle_System.copy_dir(database_dir, database_target_dir, direct = true) + Find_Facts.make_database(database_target, database_dir) Isabelle_System.rm_tree(database_dir) database_dir.dir.file.delete // "$FIND_FACTS_HOME_USER/solr" diff -r dd28f282ddc2 -r cbe937aa5e90 src/Pure/Admin/component_find_facts_web.scala --- a/src/Pure/Admin/component_find_facts_web.scala Fri Feb 28 13:50:38 2025 +0000 +++ b/src/Pure/Admin/component_find_facts_web.scala Mon Mar 03 19:52:18 2025 +0100 @@ -103,8 +103,9 @@ Sources can be found in $FIND_FACTS_HOME/web. + Fabian Huch -""") + """ + Date.Format.date(Date.now()) + "\n") /* pre-compiled web app */ diff -r dd28f282ddc2 -r cbe937aa5e90 src/Pure/GUI/rich_text.scala --- a/src/Pure/GUI/rich_text.scala Fri Feb 28 13:50:38 2025 +0000 +++ b/src/Pure/GUI/rich_text.scala Mon Mar 03 19:52:18 2025 +0100 @@ -88,15 +88,16 @@ if (cache.table == null) run else { val x = Cache.Args(msg, margin, metric) - cache.table.get(x) match { - case ref: WeakReference[Any] => ref.get.asInstanceOf[Formatted] - case null => - val y = run - cache.table.synchronized { - if (cache.table.get(x) == null) cache.table.put(x, new WeakReference[Any](y)) - } - y - } + + def get: Option[Formatted] = + cache.table.get(x) match { + case ref: WeakReference[Any] => Option(ref.get.asInstanceOf[Formatted]) + case null => None + } + + val y = get.getOrElse(run) + cache.table.synchronized { if (get.isEmpty) cache.table.put(x, new WeakReference[Any](y)) } + y } } } diff -r dd28f282ddc2 -r cbe937aa5e90 src/Tools/Find_Facts/etc/settings --- a/src/Tools/Find_Facts/etc/settings Fri Feb 28 13:50:38 2025 +0000 +++ b/src/Tools/Find_Facts/etc/settings Mon Mar 03 19:52:18 2025 +0100 @@ -3,8 +3,8 @@ FIND_FACTS_HOME="$COMPONENT" FIND_FACTS_HOME_USER="$ISABELLE_HOME_USER/find_facts" -if [ -d "$FIND_FACTS_HOME/lib/find_facts-isabelle" ]; then - FIND_FACTS_INDEXES="$FIND_FACTS_HOME/lib/find_facts-isabelle" +if [ -f "$FIND_FACTS_HOME/lib/isabelle.db" ]; then + FIND_FACTS_INDEXES="$FIND_FACTS_HOME/lib/isabelle.db" else FIND_FACTS_INDEXES="" fi diff -r dd28f282ddc2 -r cbe937aa5e90 src/Tools/Find_Facts/src/elm.scala --- a/src/Tools/Find_Facts/src/elm.scala Fri Feb 28 13:50:38 2025 +0000 +++ b/src/Tools/Find_Facts/src/elm.scala Mon Mar 03 19:52:18 2025 +0100 @@ -53,18 +53,19 @@ JSON.strings(definition, "source-directories").getOrElse( error("Missing source directories in elm.json")) - def sources: List[JFile] = + def sources: List[Path] = for { src_dir <- src_dirs path = dir + Path.explode(src_dir) file <- File.find_files(path.file, _.getName.endsWith(".elm")) - } yield file + rel_path <- File.relative_path(dir, File.path(file)) + } yield rel_path def sources_shasum: SHA1.Shasum = { val meta_info = SHA1.shasum_meta_info(SHA1.digest(JSON.Format(definition))) val head_digest = SHA1.shasum(SHA1.digest(XML.string_of_body(head)), "head") val source_digest = - SHA1.shasum_sorted(for (file <- sources) yield SHA1.digest(file) -> file.getCanonicalPath) + SHA1.shasum_sorted(for (src <- sources) yield SHA1.digest(dir + src) -> src.implode) meta_info ::: head_digest ::: source_digest } diff -r dd28f282ddc2 -r cbe937aa5e90 src/Tools/Find_Facts/src/find_facts.scala --- a/src/Tools/Find_Facts/src/find_facts.scala Fri Feb 28 13:50:38 2025 +0000 +++ b/src/Tools/Find_Facts/src/find_facts.scala Mon Mar 03 19:52:18 2025 +0100 @@ -761,13 +761,23 @@ /** index components **/ - def resolve_indexes(solr: Solr.System): Unit = - for { - path <- Path.split(Isabelle_System.getenv("FIND_FACTS_INDEXES")) - database = Library.perhaps_unprefix("find_facts-", path.file_name) - database_dir = solr.database_dir(database) - if !database_dir.is_dir - } Isabelle_System.copy_dir(path, database_dir, direct = true) + def resolve_indexes(solr: Solr.System, progress: Progress = new Progress): Unit = { + val compress_cache = Compress.Cache.make() + for (path <- Path.split(Isabelle_System.getenv("FIND_FACTS_INDEXES"))) { + val database = path.drop_ext.file_name + val database_dir = solr.database_dir(database) + if (!database_dir.is_dir) { + progress.echo("Extracting " + path.expand) + Isabelle_System.make_directory(database_dir) + File_Store.database_extract(path, database_dir, compress_cache = compress_cache) + } + } + } + + def make_database(database_path: Path, database_dir: Path): Unit = + File_Store.make_database(database_path, database_dir, + compress_options = Compress.Options_Zstd(level = 8), + compress_cache = Compress.Cache.make()) def find_facts_index_build( database: String, @@ -776,13 +786,15 @@ ): Unit = { val solr = Solr.init(solr_data_dir) - val component = "find_facts-" + database + val component = "find_facts_" + database + "-" + Date.Format.alt_date(Date.now()) val component_dir = Components.Directory(target_dir + Path.basic(component)).create(progress = progress) - Isabelle_System.copy_dir(solr.database_dir(database), component_dir.path) + val database_path = Path.basic(database).db + make_database(component_dir.path + database_path, solr.database_dir(database)) + component_dir.write_settings( - "\nFIND_FACTS_INDEXES=\"$FIND_FACTS_INDEXES:$COMPONENT/" + database + "\"") + "\nFIND_FACTS_INDEXES=\"$FIND_FACTS_INDEXES:$COMPONENT/" + database_path.implode + "\"") } @@ -993,7 +1005,7 @@ val web_assets = load_web_assets val solr = Solr.init(solr_data_dir) - resolve_indexes(solr) + resolve_indexes(solr, progress = progress) using(solr.open_database(database)) { db => val stats = Find_Facts.query_stats(db, Query(Nil))