| Author | Object | Transaction | Date |
|---|
| makarius | rISABELLEc5512fde6ad1: unused; | | Apr 12 2021, 10:17 PM |
| makarius | rISABELLEbdba138d462d: clarified signature: more structured arguments, notably for remote provers; | | Apr 12 2021, 10:16 PM |
| makarius | rISABELLE355af2d1b817: clarified signature; | | Apr 12 2021, 9:48 PM |
| makarius | rISABELLE4e6b31ed7197: clarified signature: avoid tmp file; | | Apr 12 2021, 6:29 PM |
| makarius | rISABELLE1aa92bc4d356: clarified signature for Scala functions; | | Apr 12 2021, 6:10 PM |
| dcjm | rPOLYML763128724bcf: Fix matching in allocator. | | Apr 12 2021, 3:28 PM |
| makarius | rISABELLEa021bb558feb: clarified message output: flush already happens in write_message_yxml (see… | | Apr 12 2021, 3:00 PM |
| makarius | rISABELLE55b66a45bc94: tuned; | | Apr 12 2021, 2:14 PM |
| dcjm | rPOLYML6650c5064b89: Add a cast to quieten warning. | | Apr 12 2021, 1:30 PM |
| dcjm | rPOLYMLa28fbebcee64: Add the name of the entry point to the Fail exception packet. | | Apr 12 2021, 1:30 PM |
| makarius | rISABELLEc5a390b9ae00: clarified cache; | | Apr 12 2021, 12:32 PM |
| makarius | rISABELLEc83152933579: clarified signature: Bytes extends CharSequence already (see d201996f72a8); | | Apr 12 2021, 12:16 PM |
| makarius | rISABELLEa578ebf5b78d: clarified exceptions; | | Apr 12 2021, 11:45 AM |
| makarius | rISABELLE22b5ecb53dd9: more uniform use of Byte_Message; | | Apr 11 2021, 10:47 PM |
| makarius | rISABELLEa5d1d1e2f109: tuned signature; | | Apr 11 2021, 9:32 PM |
| makarius | rISABELLE225486d9c960: tuned signature; | | Apr 11 2021, 9:23 PM |
| dcjm | rPOLYML019581b4078e: Remove no_pie option for Mac OS. We're now generating position-independent… | | Apr 11 2021, 8:00 PM |
| dcjm | rPOLYML12ad95001568: Only try with MAP_JIT trying to allocate fails without it. Earlier versions | | Apr 11 2021, 7:53 PM |
| dcjm | rPOLYMLf8727e8abf32: Comment about displaying constant areas. | | Apr 11 2021, 6:49 PM |
| dcjm | rPOLYML8cbecc5e5103: Implement relocation for the address of the constants relative to the code. | | Apr 11 2021, 6:48 PM |
| dcjm | rPOLYMLa4116d1874f4: Fix ARM64 ADRP/LDR relocations for PECOFF. | | Apr 11 2021, 6:47 PM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFPb48d456f9336: merge | | Apr 11 2021, 10:26 AM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFP70ac843c069d: increased timeout | | Apr 11 2021, 10:26 AM |
| florian.haftmann | rAFPbf1f2a489b41: collected combinatorial material | | Apr 11 2021, 9:35 AM |
| florian.haftmann | rISABELLE92783562ab78: collected combinatorial material | | Apr 11 2021, 9:35 AM |
| dcjm | rPOLYML228263573fa2: Implement relocations for ARM64 on Mac OS. Two small fixes for 32-in-64. | | Apr 11 2021, 9:21 AM |
| makarius | rISABELLE192bcee4f8b8: more robust treatment of empty markup: it allows to produce formal chunks; | | Apr 10 2021, 9:50 PM |
| makarius | rISABELLEc973b5300025: tuned; | | Apr 10 2021, 8:22 PM |
| makarius | rISABELLEb35ef8162807: tuned; | | Apr 10 2021, 7:45 PM |
| makarius | rISABELLE08bef311d382: more documentation; | | Apr 10 2021, 2:56 PM |
| makarius | rISABELLE53c148e39819: proper treatment of nested antiquotations; | | Apr 10 2021, 2:55 PM |
| dcjm | rPOLYML04d28dfd1205: Add space for UDF instruction. Don't scan code when interpreting. | | Apr 10 2021, 1:33 PM |
| makarius | rISABELLE2f6855142a8c: support for ML special forms: modified evaluation similar to Scheme; | | Apr 9 2021, 10:06 PM |
| makarius | rISABELLEa2c589d5e1e4: clarified signature: more detailed token positions for antiquotations; | | Apr 9 2021, 9:07 PM |
| dcjm | rPOLYMLa7547a5cc9ca: Implement splitting of the constant area from code for ARM64. This is… | | Apr 9 2021, 6:23 PM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFP7762d8091ebc: consolidated metadata of Anthony Bordg, metadata for new Grothendieck entry +… | | Apr 9 2021, 3:28 PM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFPd6ecd2356690: new entry: Grothendieck_Schemes | | Apr 9 2021, 11:54 AM |
| Asta Halkjær From <andro.from@gmail.com> | rAFP0fa3d918ef8c: Update root.tex | | Apr 9 2021, 11:45 AM |
| Asta Halkjær From <andro.from@gmail.com> | rAFP285e1cc62c43: Cut out Fitting's consistency properties | | Apr 9 2021, 11:35 AM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFPcf0a3199f4e7: fixed proof | | Apr 9 2021, 10:57 AM |
| makarius | rISABELLEa7aabdf889b7: clarified signature; | | Apr 8 2021, 9:09 PM |
| makarius | rAFP107ecc8216a8: clarified message, following Isabelle/a7aabdf889b7; | | Apr 8 2021, 9:09 PM |
| makarius | rISABELLEc54a9395ad96: merged | | Apr 8 2021, 8:52 PM |
| makarius | rAFP107ecc8216a8: clarified message, following Isabelle/a7aabdf889b7; | | Apr 8 2021, 4:53 PM |
| makarius | rISABELLEa7aabdf889b7: clarified signature; | | Apr 8 2021, 4:43 PM |
| florian.haftmann | rAFPc351b9b63b58: confluent preprocessing for floats in presence of target language numerals | | Apr 8 2021, 2:38 PM |
| florian.haftmann | rISABELLE7cb3fefef79e: confluent preprocessing for floats in presence of target language numerals | | Apr 8 2021, 2:38 PM |
| dcjm | rPOLYML88612786ed8c: Add a no-op after references to the constant area to allow for patching and put… | | Apr 8 2021, 1:34 PM |
| dcjm | rPOLYML726446833d1a: Merge branch 'SeparateCodeAndConsts' into ARM64Merge | | Apr 8 2021, 12:29 PM |
| makarius | rISABELLE79761915770c: some tinkering with npm versions; | | Apr 7 2021, 10:32 PM |
| makarius | rISABELLEf8c6c45cb112: some tinkering with npm versions; | | Apr 7 2021, 10:28 PM |
| makarius | rISABELLEe4fde6b3e09a: back to post-release mode; | | Apr 7 2021, 6:13 PM |
| makarius | rISABELLE1240abf2e3f5: tuned signature; | | Apr 7 2021, 6:05 PM |
| makarius | rISABELLEa69197959ab6: auto-update due to "isabelle build_vscode"; | | Apr 7 2021, 6:05 PM |
| makarius | rISABELLEf800f8becbfb: tuned; | | Apr 7 2021, 6:04 PM |
| makarius | rISABELLE80db0d2759b5: tuned --- following hints by IntelliJ IDEA; | | Apr 7 2021, 6:04 PM |
| florian.haftmann | rAFPb3ff22dfc82d: subclass relation | | Apr 7 2021, 5:46 PM |
| florian.haftmann | rISABELLEfc72e5ebf9de: subclass relation | | Apr 7 2021, 5:46 PM |
| pruvisto | rAFPc81dd066bd29: adapted to isabelle-dev/56db8559eadb | | Apr 7 2021, 5:30 PM |
| dcjm | rPOLYMLb7ca6d69fd62: Handle all cases in the switch rather than setting the value beforehand. | | Apr 7 2021, 2:38 PM |
| dcjm | rPOLYMLb3c9ae2f0331: Move GetConstSegmentForCode and related functions in MachineDependent. | | Apr 7 2021, 2:34 PM |
| florian.haftmann | rAFPeb11506f9cf9: simplified definition | | Apr 7 2021, 2:28 PM |
| florian.haftmann | rISABELLE5131c388a9b0: simplified definition | | Apr 7 2021, 2:28 PM |
| dcjm | rPOLYMLd0caa6e63c0e: Remove default heap size from bootstrap build. | | Apr 7 2021, 2:00 PM |
| dcjm | rPOLYML4cada630adb0: When splitting constants from code put them into the code area so they are… | | Apr 7 2021, 1:59 PM |
| pruvisto | rISABELLE56db8559eadb: fixed problematic addition operation in the 'approximation' package (previous… | | Apr 7 2021, 11:05 AM |
| florian.haftmann | rISABELLE0f33c7031ec9: new lemmas | | Apr 6 2021, 8:12 PM |
| florian.haftmann | rAFP63ca4e334ffc: new lemmas | | Apr 6 2021, 8:12 PM |
| nipkow | rAFPd552c27edab9: probable fix suggested by Cornelius for the changes in the vicinity of… | | Apr 6 2021, 10:15 AM |
| nipkow | rISABELLE2cd23d587db9: further clarification of Isabelle distribution identification -- avoid odd… | | Apr 6 2021, 10:15 AM |
| nipkow | rAFPd552c27edab9: probable fix suggested by Cornelius for the changes in the vicinity of… | | Apr 6 2021, 10:11 AM |
| makarius | rISABELLEe7fb17bca374: discontinue old Ubuntu 18.04 LTS, e.g. it cannot build documentation "prog… | | Apr 5 2021, 10:46 PM |
| makarius | rISABELLE543d5539306d: following recent Phabricator update, after 2021 Week 13 (Late March); | | Apr 5 2021, 10:45 PM |
| dcjm | rPOLYMLf368cd58b74c: Fix work-around when it's not needed. | | Apr 5 2021, 2:25 PM |
| dcjm | rPOLYMLccb106eca254: Work around for apparent bug in Mac OS. Reading directly into | | Apr 5 2021, 2:19 PM |
| dcjm | rPOLYMLb4b63a0583cd: #undef WORDS_BIGENDIAN in the Windows config.h since it's always little-endian. | | Apr 4 2021, 7:41 PM |
| dcjm | rPOLYML84d1d4306a57: Use the autoconf endian macro rather than trying to work out the endianness. | | Apr 4 2021, 2:57 PM |
| dcjm | rPOLYMLdaf32268d5b7: Use MAP_JIT on the initial mmap but then use mprotect to create the pages in 32… | | Apr 4 2021, 2:14 PM |
| dcjm | rPOLYML0d273b2dc831: Mac OS fixes, primarily to do with write access to executable memory. | | Apr 3 2021, 2:33 PM |
| nipkow | rAFP9ce1745d994d: Fixes due to new order prover | | Apr 3 2021, 2:17 PM |
| dcjm | rPOLYML5d9b1e2b2920: Avoid warnings with anonymous semaphores in MacOS. | | Apr 3 2021, 12:44 PM |
| dcjm | rPOLYMLf2c07e37af51: Rebuild config files after change to configure.ac. | | Apr 3 2021, 12:29 PM |
| dcjm | rPOLYML0c3a944f0495: MacOS reports the host as "arm" not "arm64". Add detection for… | | Apr 3 2021, 12:27 PM |
| dcjm | rPOLYML582f4aaa4d3e: Missed one item in previous commit. | | Apr 3 2021, 12:19 PM |
| dcjm | rPOLYML52ac604bd5cb: Fix cache clear in Mac OS. Add underscores to assembly code functions if… | | Apr 2 2021, 1:56 PM |
| paulson | rISABELLE5fa2e2786ecf: merged | | Apr 2 2021, 1:24 PM |
| paulson <lp15@cam.ac.uk> | rISABELLEc89922715bf5: Cosmetic: no !! in the lemma statement | | Apr 2 2021, 1:24 PM |
| dcjm | rPOLYMLda68b7a59168: Add ARM64 to mach-o export. | | Apr 2 2021, 1:03 PM |
| dcjm | rPOLYML856f95b35889: Don't try sem_init and sem_destroy on Mac OS X, they're deprecated. | | Apr 2 2021, 12:57 PM |
| dcjm | rPOLYML18b839f218d0: Only check range of int and unsigned if necessary. | | Apr 2 2021, 12:43 PM |
| makarius | rISABELLE04cb7e02ca38: split library index into templates | | Apr 1 2021, 7:41 PM |
| makarius | rISABELLEc337c798f64c: clarified HTML template (see also 04cb7e02ca38): avoid odd patching of sources; | | Apr 1 2021, 7:41 PM |
| makarius | rISABELLE89cf7c903aca: clarified README; | | Apr 1 2021, 7:14 PM |
| makarius | rISABELLEcf1a1e92bf34: more standard header, with utf-8 encoding; | | Apr 1 2021, 7:07 PM |
| makarius | rISABELLEc337c798f64c: clarified HTML template (see also 04cb7e02ca38): avoid odd patching of sources; | | Apr 1 2021, 7:01 PM |
| paulson <lp15@cam.ac.uk> | rAFP589a6dadfa84: another broken proof | | Apr 1 2021, 3:11 PM |
| dcjm | rPOLYMLe93546383bfd: Use SBFX for LargeWord.fromInt in 32-in-64. This untags and sign-extends in a… | | Apr 1 2021, 2:02 PM |
| Andreas Lochbihler <mail@andreas-lochbihler.de> | rAFP9a7c7db7a492: metadata for IFC_Tracking | | Apr 1 2021, 12:04 PM |
| Andreas Lochbihler <mail@andreas-lochbihler.de> | rAFP5b0b84d45ce8: new entry IFC_Tracking | | Apr 1 2021, 11:58 AM |
| paulson <lp15@cam.ac.uk> | rAFP3b2637ae2d8c: Fixed and simplified some failing proofs | | Apr 1 2021, 11:48 AM |