Page MenuHomeIsabelle/Phabricator
Feed All Transactions
AuthorObjectTransactionDate
makariusrISABELLEbf377e10ff3b: database performance tuning: prefer light-weight IPC over heavy-duty…Sun, Feb 25, 8:40 PM
makariusrISABELLEdf4eb4b05ecd: tuned signature;Sun, Feb 25, 8:13 PM
makariusrISABELLE529a6e35aaa9: tuned signature: follow PostgreSQL syntax instead of JDBC API;Sun, Feb 25, 6:47 PM
makariusrISABELLE621676d7fb9a: more robust shutdown: interruptible database connection;Sun, Feb 25, 2:53 PM
makariusrISABELLEabb5eedfeecf: clarified signature: more convenient send/receive operations;Sun, Feb 25, 1:17 PM
makariusrISABELLE54d0f6edfe3a: clarified versions for documentation;Sat, Feb 24, 10:56 PM
makariusrISABELLE32ca3d1283de: clarified signature: Build_Process tells how to clean sessions;Sat, Feb 24, 10:22 PM
makariusrISABELLEe59d93da9109: removed unused database_server (amending 32ca3d1283de);Sat, Feb 24, 10:22 PM
makariusrISABELLEaa77ebb2dc16: mergedSat, Feb 24, 10:15 PM
makariusrISABELLE5938158733bb: clarified signature: avoid hardwired values;Sat, Feb 24, 10:10 PM
makariusrISABELLEa5629eade476: clarified IPC via database server: receive notifications quasi-spontaneously…Sat, Feb 24, 10:07 PM
makariusrISABELLEdeb3056ed823: minor performance tuning: just 1 transaction for slices <= 1;Sat, Feb 24, 4:30 PM
makariusrISABELLE8544f1045123: tuned;Sat, Feb 24, 3:10 PM
nipkowrISABELLE80cb54976c1c: timing function generation bug fix by Jonas StahlSat, Feb 24, 11:29 AM
makariusrISABELLEfba02e281b44: tuned whitespace;Sat, Feb 24, 11:27 AM
makariusrISABELLEda4e82434985: tuned signature;Sat, Feb 24, 11:05 AM
makariusrISABELLEf33d37c171a9: clarified signature: fewer warnings in IntelliJ IDEA;Sat, Feb 24, 10:55 AM
makariusrISABELLEe59d93da9109: removed unused database_server (amending 32ca3d1283de);Sat, Feb 24, 10:21 AM
makariusrISABELLEd3a26436e679: tuned signature: more types, fewer warnings in IntelliJ IDEA;Fri, Feb 23, 5:22 PM
blanchetterISABELLE658f17274845: new less ad hoc implementation of the 'moura' tactic for skolemizationFri, Feb 23, 9:11 AM
makariusrISABELLE5044f1d9196d: more thorough Store.clean_output (amending 1fa1b32b0379);Thu, Feb 22, 10:07 PM
makariusrISABELLE1fa1b32b0379: build local log_db, with store/restore via optional database server;Thu, Feb 22, 10:07 PM
makariusrISABELLE5044f1d9196d: more thorough Store.clean_output (amending 1fa1b32b0379);Thu, Feb 22, 9:42 PM
makariusrISABELLE32ca3d1283de: clarified signature: Build_Process tells how to clean sessions;Thu, Feb 22, 9:28 PM
makariusrISABELLE90fbcdafb34e: clarified signature;Thu, Feb 22, 9:03 PM
makariusrISABELLEf25a6b4c3e41: tuned;Thu, Feb 22, 8:54 PM
makariusrISABELLE4ded6d260db0: tuned;Thu, Feb 22, 8:37 PM
makariusrISABELLE4f218e6e9d23: minor performance tuning;Thu, Feb 22, 8:05 PM
makariusrISABELLEa6dc0d4ffea2: tuned;Thu, Feb 22, 7:58 PM
makariusrISABELLE7a1153c95bf9: clarifier worker vs. master, which may coincide for local build;Thu, Feb 22, 5:46 PM
makariusrISABELLE1cd5888ec05f: tuned, following 7a1153c95bf9;Thu, Feb 22, 5:46 PM
makariusrISABELLE512d701d0df9: tuned signature;Thu, Feb 22, 5:24 PM
makariusrISABELLE1cd5888ec05f: tuned, following 7a1153c95bf9;Thu, Feb 22, 5:21 PM
makariusrISABELLE1fa1b32b0379: build local log_db, with store/restore via optional database server;Thu, Feb 22, 5:06 PM
makariusrISABELLEb88d73810b50: recover "build_database_server" from 1fa1b32b0379: still required, e.g. in…Thu, Feb 22, 5:06 PM
makariusrISABELLE0cac7e3634d0: more explicit build_cluster flag to guard open_build_database server;Thu, Feb 22, 5:06 PM
makariusrISABELLEba2c43592f35: proper treatment of "isabelle build_process -C" (amending 0cac7e3634d0);Thu, Feb 22, 5:06 PM
makariusrISABELLE611587256801: mergedThu, Feb 22, 4:31 PM
makariusrISABELLEe8122e84aa58: tuned signature: fewer warnings in IntelliJ IDEA;Thu, Feb 22, 2:51 PM
blanchetterAFP9fe22db3f8a8: simplified proofsThu, Feb 22, 2:20 PM
makariusrISABELLEaeb53334f521: proper usage;Thu, Feb 22, 2:17 PM
blanchetterAFPf47a01e6ab6d: simplified proofThu, Feb 22, 2:14 PM
makariusrISABELLEb88d73810b50: recover "build_database_server" from 1fa1b32b0379: still required, e.g. in…Thu, Feb 22, 2:08 PM
makariusrISABELLEb676998d7f97: clarified signature;Thu, Feb 22, 1:57 PM
makariusrISABELLE2e1f75c870e3: more robust: make double-sure that heap digest is present;Thu, Feb 22, 1:27 PM
makariusrISABELLEa2256e4a77bf: tuned;Thu, Feb 22, 1:24 PM
makariusrISABELLEeb742d4e4dc9: minor performance tuning: just one transaction for log_db without heap;Thu, Feb 22, 1:19 PM
makariusrISABELLEab7ec4a29b9c: tuned;Thu, Feb 22, 1:12 PM
makariusrISABELLE909031707ff4: proper store.cache.compress;Thu, Feb 22, 1:00 PM
makariusrISABELLE3f307faf9111: tuned whitespace;Thu, Feb 22, 12:57 PM
makariusrISABELLEd298c5b65d8e: clarified store_session: heap requires process_result.ok, but log_db is always…Thu, Feb 22, 12:53 PM
makariusrISABELLEecc851dd274f: unused;Thu, Feb 22, 12:22 PM
makariusrISABELLEfabe9f89911f: tuned;Thu, Feb 22, 12:19 PM
makariusrISABELLE3abfc5ebabad: tuned names;Thu, Feb 22, 12:14 PM
makariusrISABELLE48628d2e30ef: tuned names;Thu, Feb 22, 11:52 AM
makariusrISABELLEd2cb610c4229: clarified database layout;Wed, Feb 21, 8:37 PM
makariusrISABELLE45af93b0370a: tuned signature;Wed, Feb 21, 8:21 PM
makariusrISABELLE0554a32a6ef4: clarified signature;Wed, Feb 21, 7:59 PM
makariusrISABELLEade429ddb1fc: more accurate types;Wed, Feb 21, 7:54 PM
makariusrISABELLE1fa1b32b0379: build local log_db, with store/restore via optional database server;Wed, Feb 21, 7:36 PM
paulson <lp15@cam.ac.uk>rAFPdfb6d84bb6c5: Incorporating library material from AFP sessionsWed, Feb 21, 7:03 PM
florian.haftmannrISABELLEc172eecba85d: simplified specification of type class semiring_bitsWed, Feb 21, 5:19 PM
paulson <lp15@cam.ac.uk>rISABELLE76720aeab21e: New material about transcendental functions, polynomials, et cetera, thanks to…Wed, Feb 21, 11:46 AM
makariusrISABELLEdf1059ea8846: propagate property "isabelle.debug", notably for Java/Scala exception trace;Wed, Feb 21, 11:43 AM
blanchetterAFP91e281be1e8f: avoid noncanonical uses of 'moura' tactic ahead of new implementation of tacticTue, Feb 20, 2:21 PM
paulsonrAFPac72f2262471: merged
paulson committed rAFPac72f2262471: merged. 
Tue, Feb 20, 1:51 PM
paulson <lp15@cam.ac.uk>rAFP3eebb590ad05: Removed numerous z3 calls and tried to simplify some extremely messy proofsTue, Feb 20, 1:51 PM
paulson <lp15@cam.ac.uk>rAFP5bd0cbadc628: Adjustments for recent changes to the main repositoryTue, Feb 20, 1:46 PM
blanchetterAFP1b0a95af1620: avoid noncanonical uses of 'moura' tactic ahead of new implementation of tacticTue, Feb 20, 9:15 AM
paulson <lp15@cam.ac.uk>rAFP12696f4c5610: A little tidying up. Removed some smt callsMon, Feb 19, 4:34 PM
makariusrISABELLE0b58e85906a1: tuned;Mon, Feb 19, 4:25 PM
makariusrISABELLEba2c43592f35: proper treatment of "isabelle build_process -C" (amending 0cac7e3634d0);Mon, Feb 19, 4:04 PM
blanchetterAFP72cce11020f9: tuned proofsMon, Feb 19, 3:46 PM
paulsonrISABELLE1d0cb3f003d4: merged
paulson committed rISABELLE1d0cb3f003d4: merged. 
Mon, Feb 19, 3:12 PM
paulson <lp15@cam.ac.uk>rISABELLEf471e1715fc4: A small collection of new and useful facts, including the AM-GM inequalityMon, Feb 19, 3:12 PM
blanchetterISABELLEa3e7a323780f: remove selected occurrences of 'moura' tacticMon, Feb 19, 2:31 PM
makariusrISABELLE5979ba127524: clarified signature;Mon, Feb 19, 11:47 AM
makariusrISABELLE49370f0f7911: clarified names;Mon, Feb 19, 11:39 AM
desharnarISABELLE9f36a31fe7ae: added lemmas relpowp_left_unique and relpow_left_uniqueMon, Feb 19, 11:39 AM
makariusrISABELLE0cac7e3634d0: more explicit build_cluster flag to guard open_build_database server;Mon, Feb 19, 11:30 AM
desharnarISABELLEd4c077078497: added lemmas relpowp_right_unique and relpow_right_uniqueMon, Feb 19, 11:21 AM
makariusrISABELLE82038b9eb89a: tuned;Mon, Feb 19, 11:07 AM
nipkowrISABELLE65223730d7e1: use define_time_funMon, Feb 19, 8:23 AM
nipkowrISABELLE0a152b2f73ae: time funs: +1 instead of 1+Sun, Feb 18, 9:35 PM
makariusrISABELLE215db9299a1a: clarified signature;Sun, Feb 18, 7:09 PM
makariusrISABELLE26fa2e8761fb: minor performance tuning;Sun, Feb 18, 3:16 PM
makariusrISABELLE4a299bdb5d61: clarified signature: more comprehensive operations;Sun, Feb 18, 3:15 PM
makariusrISABELLEdca6ea3b7a01: clarified signature: more explicit types;Sun, Feb 18, 3:03 PM
makariusrISABELLE2a9d8c74eb3c: clarified signature: emphasize physical db files;Sun, Feb 18, 1:32 PM
makariusrISABELLE49475f8bb4cc: tuned: afford untyped/unscoped update;Sun, Feb 18, 1:01 PM
makariusrISABELLEa4118f530263: clarified signature: avoid ill-defined type java.net.URL;Sun, Feb 18, 12:33 PM
makariusrISABELLE5d77df3d30d1: unused;Sun, Feb 18, 12:32 PM
kleingrAFPf5d6d7c7f38e: Simpl: remove stray thm commandSun, Feb 18, 9:56 AM
kleingrAFPc5ea13f67ee4: CRYSTALS-Kyber_Security: adapt to isabelle@cff4576218faSun, Feb 18, 5:52 AM
kleingrAFP1cb02f1980cb: Interval_Analysis: adapt to isabelle@cff4576218faSun, Feb 18, 4:21 AM
kleingrAFP3573cc4311ae: merge from afp-2023Sun, Feb 18, 3:59 AM
kleingrAFP6444261143dc: update Simpl entry; change license to BSDSun, Feb 18, 12:45 AM
makariusrISABELLEcff4576218fa: tuned: afford untyped/unscoped update;Sat, Feb 17, 9:28 PM
makariusrISABELLE10e560f2f580: more robust default: Scala imposes explicit "threads" value on ML, both the…Sat, Feb 17, 9:26 PM
makariusrISABELLE422a6e04cf0f: clarified signature: more explicit types/scopes;Sat, Feb 17, 9:21 PM