Page MenuHomeIsabelle/Phabricator

Open Tasks

Normal (6)

Wishlist (4)

Active Repositories

Recent Activity

Wed, Jan 19

desharna committed rISABELLEfc664e4fbf6d: added Mirabelle option -r to randomize the goals before selection.
added Mirabelle option -r to randomize the goals before selection
Wed, Jan 19, 9:43 AM

Tue, Jan 18

paulson <lp15@cam.ac.uk> committed rAFP81aae6b30ce5: Removal of a lemma (now in the libraries) and a few tweaks.
Removal of a lemma (now in the libraries) and a few tweaks
Tue, Jan 18, 12:52 PM
paulson <lp15@cam.ac.uk> committed rISABELLEac3901e4e0a9: A new lemma about inverse image.
A new lemma about inverse image
Tue, Jan 18, 12:13 PM

Mon, Jan 17

desharna committed rISABELLE192876ea202d: proper treatment of $let variables in symbol table in Sledgehammer.
proper treatment of $let variables in symbol table in Sledgehammer
Mon, Jan 17, 8:27 AM

Sun, Jan 16

dcjm committed rPOLYML67384d30eb85: The parent of "../.." is "../../.." not "..". Fixes #167. (authored by dcjm).
The parent of "../.." is "../../.." not "..". Fixes #167.
Sun, Jan 16, 2:18 PM
dcjm committed rPOLYML6406862e6b32: Try using the atomic operations added in ARM 8.1. These are not available in… (authored by dcjm).
Try using the atomic operations added in ARM 8.1. These are not available in…
Sun, Jan 16, 2:18 PM
dcjm committed rPOLYML1b6a34576dab: Change to use load-acquire to lock and swap-release to unlock. (authored by dcjm).
Change to use load-acquire to lock and swap-release to unlock.
Sun, Jan 16, 2:18 PM
dcjm committed rPOLYMLed5b19cb8079: Restore the spinning that was previously used to check for a mutex lock. (authored by dcjm).
Restore the spinning that was previously used to check for a mutex lock.
Sun, Jan 16, 2:18 PM
dcjm committed rPOLYMLae59fee9fd54: Disable LSE atomics for the moment. (authored by dcjm).
Disable LSE atomics for the moment.
Sun, Jan 16, 2:18 PM
dcjm committed rPOLYML354708c15aa7: Allow for the extremely unlikely situation of floating point constants in a… (authored by dcjm).
Allow for the extremely unlikely situation of floating point constants in a…
Sun, Jan 16, 2:18 PM
dcjm committed rPOLYMLee4355129523: Don't include container arguments among the "stable" arguments for non-tail… (authored by dcjm).
Don't include container arguments among the "stable" arguments for non-tail…
Sun, Jan 16, 2:18 PM
dcjm committed rPOLYMLe6117d4d84c7: Sort the constant lists to avoid duplicates. Use bit-encoding for 64-bit… (authored by dcjm).
Sort the constant lists to avoid duplicates. Use bit-encoding for 64-bit…
Sun, Jan 16, 2:18 PM
dcjm committed rPOLYML6cc00b4ea313: Use movi for floating point zero. (authored by dcjm).
Use movi for floating point zero.
Sun, Jan 16, 2:18 PM
dcjm committed rPOLYMLfd044f2c927f: Fix float constants for big-endian. (authored by dcjm).
Fix float constants for big-endian.
Sun, Jan 16, 2:18 PM
dcjm committed rPOLYMLeb2ed058d3b3: Implement floating point constants in the non-address area. (authored by dcjm).
Implement floating point constants in the non-address area.
Sun, Jan 16, 2:18 PM
dcjm committed rPOLYMLdfc2227eee20: Remove CheckRTSException; add back CPUPause. (authored by dcjm).
Remove CheckRTSException; add back CPUPause.
Sun, Jan 16, 2:18 PM
dcjm committed rPOLYML1a120b3f9145: Added load/storePolyWord/NativeWord functions to RunCall. (authored by dcjm).
Added load/storePolyWord/NativeWord functions to RunCall.
Sun, Jan 16, 2:18 PM
dcjm committed rPOLYMLf12e7ed29c45: Use TBZ/TBNZ for tag test and branches. (authored by dcjm).
Use TBZ/TBNZ for tag test and branches.
Sun, Jan 16, 2:18 PM
dcjm committed rPOLYML0c294ecf45e8: Move code to check for RTS exceptions into the RTS caller for the X86. This… (authored by dcjm).
Move code to check for RTS exceptions into the RTS caller for the X86. This…
Sun, Jan 16, 2:18 PM
dcjm committed rPOLYMLc6b4f0156a86: Combine adjacent pushes, combine stack resets and use post-indexing to include… (authored by dcjm).
Combine adjacent pushes, combine stack resets and use post-indexing to include…
Sun, Jan 16, 2:18 PM
dcjm committed rPOLYML66ee38bacc6f: Use ldp and stp for adjacent loads and stores where possible. (authored by dcjm).
Use ldp and stp for adjacent loads and stores where possible.
Sun, Jan 16, 2:18 PM
dcjm committed rPOLYML8972ed6ab731: Begin peep-hole optimisation. Eliminate unnecessary branches and straighten… (authored by dcjm).
Begin peep-hole optimisation. Eliminate unnecessary branches and straighten…
Sun, Jan 16, 2:18 PM
dcjm committed rPOLYML19394e9731c1: Handle allocations of > 4096 which was omitted in earlier change. (authored by dcjm).
Handle allocations of > 4096 which was omitted in earlier change.
Sun, Jan 16, 2:18 PM
dcjm committed rPOLYML7f766f218d7d: Move allocation code and branch tables into pre-assembler "instructions". (authored by dcjm).
Move allocation code and branch tables into pre-assembler "instructions".
Sun, Jan 16, 2:17 PM
dcjm committed rPOLYML780cd89c9301: Convert ForeignCall to use the pre-assembler layer. Remove ArmSequences and… (authored by dcjm).
Convert ForeignCall to use the pre-assembler layer. Remove ArmSequences and…
Sun, Jan 16, 2:17 PM
dcjm committed rPOLYML4b3b81c5fe8f: Remove temporary functions that converted the pre-assembly code to the assembly… (authored by dcjm).
Remove temporary functions that converted the pre-assembly code to the assembly…
Sun, Jan 16, 2:17 PM
dcjm committed rPOLYML417c12dbd538: Return small numbers of multiple results in registers. (authored by dcjm).
Return small numbers of multiple results in registers.
Sun, Jan 16, 2:17 PM
dcjm committed rPOLYML0a5ebb0e3f7c: Fix another case where the optimiser added a new tuple but didn't set the… (authored by dcjm).
Fix another case where the optimiser added a new tuple but didn't set the…
Sun, Jan 16, 2:17 PM
dcjm committed rPOLYML0d81c03edaec: Clean up the conflict test for arguments of long format arbitrary precision… (authored by dcjm).
Clean up the conflict test for arguments of long format arbitrary precision…
Sun, Jan 16, 2:17 PM
dcjm committed rPOLYML8c171e2fdd8d: Support for multiple results from function calls. (authored by dcjm).
Support for multiple results from function calls.
Sun, Jan 16, 2:17 PM
dcjm committed rPOLYML90195d19db1a: Don't attempt to merge cache states for the moment. It seems to be broken. (authored by dcjm).
Don't attempt to merge cache states for the moment. It seems to be broken.
Sun, Jan 16, 2:17 PM
dcjm committed rPOLYML4c9b9ada1d9c: Fix the optimiser so that it sets the correct argument type for newly… (authored by dcjm).
Fix the optimiser so that it sets the correct argument type for newly…
Sun, Jan 16, 2:17 PM
dcjm committed rPOLYMLb9af39e4fe02: Use hints to improve the chances that we will be able to retain cache states… (authored by dcjm).
Use hints to improve the chances that we will be able to retain cache states…
Sun, Jan 16, 2:17 PM
dcjm committed rPOLYMLae887f45ad23: Add a dummy instruction if we're caching to see if this is the problem. (authored by dcjm).
Add a dummy instruction if we're caching to see if this is the problem.
Sun, Jan 16, 2:17 PM
dcjm committed rPOLYMLf4d7485ce35f: Fix incorrect test. (authored by dcjm).
Fix incorrect test.
Sun, Jan 16, 2:17 PM
dcjm committed rPOLYMLbbfb606f0d84: Use an indexed load in 32-in-64 if the offset is zero and this is the last… (authored by dcjm).
Use an indexed load in 32-in-64 if the offset is zero and this is the last…
Sun, Jan 16, 2:17 PM
dcjm committed rPOLYML6ad5898ed17b: Merge the cache state on multiple paths. (authored by dcjm).
Merge the cache state on multiple paths.
Sun, Jan 16, 2:17 PM
dcjm committed rPOLYMLaceade0631e0: Include the cache registers in the save mask for allocations so that if there… (authored by dcjm).
Include the cache registers in the save mask for allocations so that if there…
Sun, Jan 16, 2:17 PM
dcjm committed rPOLYMLbebfbd0bd69a: Change the assertion into a test and don't optimise if the result of the load… (authored by dcjm).
Change the assertion into a test and don't optimise if the result of the load…
Sun, Jan 16, 2:17 PM
dcjm committed rPOLYML4c0882484f03: Cache the combination of loading a value from the stack and getting the… (authored by dcjm).
Cache the combination of loading a value from the stack and getting the…
Sun, Jan 16, 2:17 PM