Page MenuHomeIsabelle/Phabricator
Feed All Stories

Today

paulson committed rISABELLEa9aaef9fcf86: merged.
merged
Tue, Oct 20, 12:16 AM
paulson <lp15@cam.ac.uk> committed rISABELLE7956d958ef5b: tidying and de-applying.
tidying and de-applying
Tue, Oct 20, 12:16 AM

Yesterday

makarius created Blog Post: Update external prover components for Sledgehammer etc..
Mon, Oct 19, 5:02 PM
makarius created Blog Post: Include veriT component for "smt" method.
Mon, Oct 19, 4:59 PM
dcjm committed rPOLYML2eed06577510: Change threadId argument to FirstArgument. These were merged after the change… (authored by dcjm).
Change threadId argument to FirstArgument. These were merged after the change…
Mon, Oct 19, 12:39 PM
dcjm committed rPOLYML2dcaf593e4e7: Merge branch 'VolatileRef' into CompiledFFITesting (authored by dcjm).
Merge branch 'VolatileRef' into CompiledFFITesting
Mon, Oct 19, 12:39 PM
dcjm committed rPOLYML03c23e724928: Fix MutexBlock after change to mutex values. (authored by dcjm).
Fix MutexBlock after change to mutex values.
Mon, Oct 19, 12:39 PM
dcjm committed rPOLYML76a9c2d1321c: Minor fixes. (authored by dcjm).
Minor fixes.
Mon, Oct 19, 12:39 PM
dcjm committed rPOLYMLe4ca9570364c: Merge branch 'VolatileRef' into CompiledFFITesting (authored by dcjm).
Merge branch 'VolatileRef' into CompiledFFITesting
Mon, Oct 19, 12:39 PM
dcjm committed rPOLYML577b743e2b30: Move the creation of the atExit list up to LibrarySupport so that it can be… (authored by dcjm).
Move the creation of the atExit list up to LibrarySupport so that it can be…
Mon, Oct 19, 12:39 PM
dcjm committed rPOLYML554e9a26bbea: Fix atExit. (authored by dcjm).
Fix atExit.
Mon, Oct 19, 12:39 PM
dcjm committed rPOLYMLaff77383269a: Remove atExit functions from RTS since it's now handled entirely in ML. (authored by dcjm).
Remove atExit functions from RTS since it's now handled entirely in ML.
Mon, Oct 19, 12:39 PM
dcjm committed rPOLYML3c3179664d88: When exporting a volatile ref we can clear it if it is in hierarchy zero i.e. (authored by dcjm).
When exporting a volatile ref we can clear it if it is in hierarchy zero i.e.
Mon, Oct 19, 12:39 PM
dcjm committed rPOLYML7b258292fd45: Merge branch 'master' into ForkRTSModule (authored by dcjm).
Merge branch 'master' into ForkRTSModule
Mon, Oct 19, 12:39 PM
dcjm committed rPOLYML47edaa46b73b: Merge branch 'master' into VolatileRef (authored by dcjm).
Merge branch 'master' into VolatileRef
Mon, Oct 19, 12:39 PM
dcjm committed rPOLYMLd3b1b22f3b26: Remove ProcessExternal::SetSingleThreaded since this is handled by RtsModule… (authored by dcjm).
Remove ProcessExternal::SetSingleThreaded since this is handled by RtsModule…
Mon, Oct 19, 12:39 PM
dcjm committed rPOLYML958394264734: Add a virtual function to the RtsModules class to handle the very specific case… (authored by dcjm).
Add a virtual function to the RtsModules class to handle the very specific case…
Mon, Oct 19, 12:39 PM
dcjm committed rPOLYMLe16e73a30b45: Note a problem with clearing before exporting. The exported version of a saved… (authored by dcjm).
Note a problem with clearing before exporting. The exported version of a saved…
Mon, Oct 19, 12:39 PM
dcjm committed rPOLYML3fdba2e620c4: Use volatile refs explicitly. Convert OS.Process.atExit to use them so that it… (authored by dcjm).
Use volatile refs explicitly. Convert OS.Process.atExit to use them so that it…
Mon, Oct 19, 12:39 PM
dcjm committed rPOLYML5069d7f22b68: Clear no-overwrite word ref values when they are exported. This avoids (authored by dcjm).
Clear no-overwrite word ref values when they are exported. This avoids
Mon, Oct 19, 12:39 PM
dcjm committed rPOLYML8f3d4133c678: Change comment to reflect the changes to the code. (authored by dcjm).
Change comment to reflect the changes to the code.
Mon, Oct 19, 12:39 PM
dcjm committed rPOLYMLf5bd8f5d7ac8: Change the X86 code-generator so that resetting a mutex sets it to zero. (authored by dcjm).
Change the X86 code-generator so that resetting a mutex sets it to zero.
Mon, Oct 19, 12:39 PM
dcjm committed rPOLYML1a0edce725cc: Change the way mutexes are locked and unlocked. They are now created as zero… (authored by dcjm).
Change the way mutexes are locked and unlocked. They are now created as zero…
Mon, Oct 19, 12:39 PM
dcjm committed rPOLYML7708643e1098: Change the buildClosure functions into buildCallback functions that take the ML… (authored by dcjm).
Change the buildClosure functions into buildCallback functions that take the ML…
Mon, Oct 19, 12:39 PM
dcjm committed rPOLYMLea1d81c08167: Merge branch 'master' into CompiledFFITesting (authored by dcjm).
Merge branch 'master' into CompiledFFITesting
Mon, Oct 19, 12:39 PM
dcjm committed rPOLYML0cf2b206fec8: Merge branch 'AnotherPollBranch' into CompiledFFITesting (authored by dcjm).
Merge branch 'AnotherPollBranch' into CompiledFFITesting
Mon, Oct 19, 12:39 PM
dcjm committed rPOLYML595b0a71904d: Merge branch 'master' into AnotherPollBranch (authored by dcjm).
Merge branch 'master' into AnotherPollBranch
Mon, Oct 19, 12:39 PM
dcjm committed rPOLYMLd88a3edcb98c: Merge branch 'master' into AnotherPollBranch (authored by dcjm).
Merge branch 'master' into AnotherPollBranch
Mon, Oct 19, 12:39 PM
dcjm committed rPOLYML04a4c1ed1756: Merge branch 'master' into AnotherPollBranch (authored by dcjm).
Merge branch 'master' into AnotherPollBranch
Mon, Oct 19, 12:39 PM
dcjm committed rPOLYML8e316fd16edd: Remove the code to make trampolines since they are no longer used. (authored by dcjm).
Remove the code to make trampolines since they are no longer used.
Mon, Oct 19, 12:38 PM
dcjm committed rPOLYML3d031d25a475: Merge branch 'CompileForeignCall' into CompliedFFITesting (authored by dcjm).
Merge branch 'CompileForeignCall' into CompliedFFITesting
Mon, Oct 19, 12:38 PM
dcjm committed rPOLYML48cb2b24ff27: Revert "Remove FlushInstructionCache" d3c42ae. We may need this for the ARM… (authored by dcjm).
Revert "Remove FlushInstructionCache" d3c42ae. We may need this for the ARM…
Mon, Oct 19, 12:38 PM
dcjm committed rPOLYMLc89f66c8ee6e: The abi type is always a short int. (authored by dcjm).
The abi type is always a short int.
Mon, Oct 19, 12:38 PM
dcjm committed rPOLYMLbbfff949ac36: Merge branch 'master' into CompileForeignCall (authored by dcjm).
Merge branch 'master' into CompileForeignCall
Mon, Oct 19, 12:38 PM
dcjm committed rPOLYML0433fa46ab63: Remove PolyInterpretedCreateCallback since we're not supporting callbacks in… (authored by dcjm).
Remove PolyInterpretedCreateCallback since we're not supporting callbacks in…
Mon, Oct 19, 12:38 PM
dcjm committed rPOLYMLf569b0e3e8ed: Fixes, mainly with structs. (authored by dcjm).
Fixes, mainly with structs.
Mon, Oct 19, 12:38 PM
dcjm committed rPOLYML03439e5b3c54: Pass a vector of addresses to ffi_call rather than the arguments themselves. (authored by dcjm).
Pass a vector of addresses to ffi_call rather than the arguments themselves.
Mon, Oct 19, 12:38 PM
dcjm committed rPOLYML32d30a3f8d98: Include a temporary version of RunCall.rtsCallFull4 because it isn't included… (authored by dcjm).
Include a temporary version of RunCall.rtsCallFull4 because it isn't included…
Mon, Oct 19, 12:38 PM
dcjm committed rPOLYML7977da2fa662: Tidy up to fix some issues. (authored by dcjm).
Tidy up to fix some issues.
Mon, Oct 19, 12:38 PM
dcjm committed rPOLYMLf91979dbb293: Raise an exception if FFI is not supported. (authored by dcjm).
Raise an exception if FFI is not supported.
Mon, Oct 19, 12:38 PM
dcjm committed rPOLYMLdc3fe8d79cbb: Added support for foreign function calling. (authored by dcjm).
Added support for foreign function calling.
Mon, Oct 19, 12:38 PM
dcjm committed rPOLYML3078ee3a3193: Add initial support for FFI in interpreted version. (authored by dcjm).
Add initial support for FFI in interpreted version.
Mon, Oct 19, 12:38 PM
dcjm committed rPOLYMLdaae1dd83d51: Merge branch 'CompileForeignCall' of https://github.com/dcjm/polyml into… (authored by dcjm).
Merge branch 'CompileForeignCall' of https://github.com/dcjm/polyml into…
Mon, Oct 19, 12:38 PM
dcjm committed rPOLYML5f27082311fa: Add configure tests for libffi and ffi.h in case we're building the interpreted… (authored by dcjm).
Add configure tests for libffi and ffi.h in case we're building the interpreted…
Mon, Oct 19, 12:38 PM
dcjm committed rPOLYML27c401732751: Added Inet6Sock and removed NetHostDB. This brings it in line for polyml.pyp. (authored by dcjm).
Added Inet6Sock and removed NetHostDB. This brings it in line for polyml.pyp.
Mon, Oct 19, 12:38 PM
dcjm committed rPOLYML3136b9e2ad76: Rename the configurations to build the interpreted versions so Debug and… (authored by dcjm).
Rename the configurations to build the interpreted versions so Debug and…
Mon, Oct 19, 12:38 PM
dcjm committed rPOLYML9f1501d89010: Turn abiList into a function so it is only constructed when initGlobalEnv is… (authored by dcjm).
Turn abiList into a function so it is only constructed when initGlobalEnv is…
Mon, Oct 19, 12:38 PM
dcjm committed rPOLYML0e4a53fdf878: Another basis file that needs a different version after the compiler has been… (authored by dcjm).
Another basis file that needs a different version after the compiler has been…
Mon, Oct 19, 12:38 PM
dcjm committed rPOLYMLa7c1ad60d382: Rebuild to incorporate changes to Makefile.am. (authored by dcjm).
Rebuild to incorporate changes to Makefile.am.
Mon, Oct 19, 12:38 PM
dcjm committed rPOLYMLd049d85ff591: Forgot to include this. (authored by dcjm).
Forgot to include this.
Mon, Oct 19, 12:38 PM
dcjm committed rPOLYML183f259793cf: Merge branch 'master' into CompileForeignCall (authored by dcjm).
Merge branch 'master' into CompileForeignCall
Mon, Oct 19, 12:38 PM
dcjm committed rPOLYMLb20f645a47d8: Update compiler version to 5.8.2 so that we pick up the correct files on… (authored by dcjm).
Update compiler version to 5.8.2 so that we pick up the correct files on…
Mon, Oct 19, 12:38 PM
dcjm committed rPOLYML659ee6b884d0: Move changed files now that the base version is 5.8.1. (authored by dcjm).
Move changed files now that the base version is 5.8.1.
Mon, Oct 19, 12:38 PM
dcjm committed rPOLYML96cac5d31cff: Rebuild configure and Makefiles after removing libffi. (authored by dcjm).
Rebuild configure and Makefiles after removing libffi.
Mon, Oct 19, 12:38 PM
dcjm committed rPOLYML9b3de2006d5d: No longer use libffi for anything. (authored by dcjm).
No longer use libffi for anything.
Mon, Oct 19, 12:38 PM
dcjm committed rPOLYML04d02b420f73: Remove libffi completely. (authored by dcjm).
Remove libffi completely.
Mon, Oct 19, 12:37 PM
dcjm committed rPOLYML7707bcf6dd7f: Switch to using the ML representation of the data structure for C types. (authored by dcjm).
Switch to using the ML representation of the data structure for C types.
Mon, Oct 19, 12:37 PM
dcjm committed rPOLYML6b111a0974e6: Use an internal representation for the ABI rather than libffi's. (authored by dcjm).
Use an internal representation for the ABI rather than libffi's.
Mon, Oct 19, 12:37 PM
dcjm committed rPOLYML6961db963d31: Create a Foreign structure in Initialise and use that when building the basis… (authored by dcjm).
Create a Foreign structure in Initialise and use that when building the basis…
Mon, Oct 19, 12:37 PM
dcjm committed rPOLYML8c6694eff2b5: Remove RTS calls from poly_ffi. (authored by dcjm).
Remove RTS calls from poly_ffi.
Mon, Oct 19, 12:37 PM
dcjm committed rPOLYMLbdbd450fbc48: Add old version for bootstrap. (authored by dcjm).
Add old version for bootstrap.
Mon, Oct 19, 12:37 PM
dcjm committed rPOLYML41b61aa395a9: Switch to using the separate RTS calls. (authored by dcjm).
Switch to using the separate RTS calls.
Mon, Oct 19, 12:37 PM
dcjm committed rPOLYMLc8403b6d1259: Complete closures for Unix 64-bit by implementing structs as arguments and… (authored by dcjm).
Complete closures for Unix 64-bit by implementing structs as arguments and…
Mon, Oct 19, 12:37 PM
dcjm committed rPOLYML3c59e5fcd416: Small fix to FFI RTS call for Unix. (authored by dcjm).
Small fix to FFI RTS call for Unix.
Mon, Oct 19, 12:37 PM
dcjm committed rPOLYML206b68f67116: Complete struct passing for Win64 callbacks. (authored by dcjm).
Complete struct passing for Win64 callbacks.
Mon, Oct 19, 12:37 PM
dcjm committed rPOLYMLfc8823656e46: Generate the main part of a callback in the first application to the argument… (authored by dcjm).
Generate the main part of a callback in the first application to the argument…
Mon, Oct 19, 12:37 PM
dcjm committed rPOLYML6214eb21b5cd: Change the way the cStructn functions work so that it is possible to compute… (authored by dcjm).
Change the way the cStructn functions work so that it is possible to compute…
Mon, Oct 19, 12:37 PM
dcjm committed rPOLYML07c9e32fcf82: Add original version of ForeignMemory for bootstrapping. (authored by dcjm).
Add original version of ForeignMemory for bootstrapping.
Mon, Oct 19, 12:37 PM
dcjm committed rPOLYML4d251dd08ab7: Use alloca for arguments and result in FFI calls. (authored by dcjm).
Use alloca for arguments and result in FFI calls.
Mon, Oct 19, 12:37 PM
dcjm committed rPOLYML4b901f4f7e85: Add Foreign.Memory.alloca. This allocates temporary memory on the stack. (authored by dcjm).
Add Foreign.Memory.alloca. This allocates temporary memory on the stack.
Mon, Oct 19, 12:37 PM
dcjm committed rPOLYML57d941372a34: Add separate RTS calls for the FFI functions. (authored by dcjm).
Add separate RTS calls for the FFI functions.
Mon, Oct 19, 12:37 PM
dcjm committed rPOLYML2f4d00556739: When passing a callback touch it in the "delete" function. (authored by dcjm).
When passing a callback touch it in the "delete" function.
Mon, Oct 19, 12:37 PM
dcjm committed rPOLYML8355901278a6: Merge branch 'master' into CompileForeignCall (authored by dcjm).
Merge branch 'master' into CompileForeignCall
Mon, Oct 19, 12:37 PM
dcjm committed rPOLYML1099f0201f17: Add comment about closures. (authored by dcjm).
Add comment about closures.
Mon, Oct 19, 12:37 PM
dcjm committed rPOLYML19cc0848c6c7: Remove assembly code entries for kill-self and pop-arg-and-closure. (authored by dcjm).
Remove assembly code entries for kill-self and pop-arg-and-closure.
Mon, Oct 19, 12:37 PM
dcjm committed rPOLYML091584201122: Add inline absolute 64-bit constants to the code-generator for 32-in-64. This… (authored by dcjm).
Add inline absolute 64-bit constants to the code-generator for 32-in-64. This…
Mon, Oct 19, 12:37 PM
dcjm committed rPOLYMLa1ba54bf3fb5: Fix argument area address in X64/Unix closures. (authored by dcjm).
Fix argument area address in X64/Unix closures.
Mon, Oct 19, 12:37 PM
dcjm committed rPOLYML0e62d5c15252: Push with 32-bit address is only used in native 32-bits. (authored by dcjm).
Push with 32-bit address is only used in native 32-bits.
Mon, Oct 19, 12:37 PM
dcjm committed rPOLYMLaffea672b056: Added support for C closures (callbacks) in Unix 64-bit. (authored by dcjm).
Added support for C closures (callbacks) in Unix 64-bit.
Mon, Oct 19, 12:37 PM
dcjm committed rPOLYML1f39763faa8b: Largely complete closures for 64-bit Windows. Structs as arguments are not yet… (authored by dcjm).
Largely complete closures for 64-bit Windows. Structs as arguments are not yet…
Mon, Oct 19, 12:37 PM
dcjm committed rPOLYML3e7dac6eb710: Convert 64-bit GAS to use RTS calls for traps. (authored by dcjm).
Convert 64-bit GAS to use RTS calls for traps.
Mon, Oct 19, 12:37 PM
dcjm committed rPOLYML74e0516db2a7: Modify assembly code for 32-bit GAS. (authored by dcjm).
Modify assembly code for 32-bit GAS.
Mon, Oct 19, 12:37 PM
dcjm committed rPOLYML39d12a6e725b: Handle KillException in the trap handler. (authored by dcjm).
Handle KillException in the trap handler.
Mon, Oct 19, 12:37 PM
dcjm committed rPOLYMLf5af1f6645ce: Change Windows 64-bit assembly code to call trap handler. (authored by dcjm).
Change Windows 64-bit assembly code to call trap handler.
Mon, Oct 19, 12:37 PM
dcjm committed rPOLYMLe1e07285e039: Switch to using compiled call-back functions. (authored by dcjm).
Switch to using compiled call-back functions.
Mon, Oct 19, 12:37 PM
dcjm committed rPOLYMLd67d74b0186d: Handle GC and stack overflow traps by calling into the C code rather than… (authored by dcjm).
Handle GC and stack overflow traps by calling into the C code rather than…
Mon, Oct 19, 12:37 PM
dcjm committed rPOLYML56e061b79c88: Save the C stack pointer when returning from a foreign call. Currently only 32… (authored by dcjm).
Save the C stack pointer when returning from a foreign call. Currently only 32…
Mon, Oct 19, 12:37 PM
dcjm committed rPOLYML237e2f9c3e3c: Switch to using the compiled call-back code. (authored by dcjm).
Switch to using the compiled call-back code.
Mon, Oct 19, 12:37 PM
dcjm committed rPOLYML184ae2dc3b21: Implement foreign callback functions for X86/32. (authored by dcjm).
Implement foreign callback functions for X86/32.
Mon, Oct 19, 12:37 PM
dcjm committed rPOLYMLf1605bb7be4d: FFI_SYSV needs to be included in X86/32 since it is the default API. (authored by dcjm).
FFI_SYSV needs to be included in X86/32 since it is the default API.
Mon, Oct 19, 12:36 PM
dcjm committed rPOLYMLcc67e4d29f7c: Fix for 32-in-64 on Unix. We can't use mlArg2Reg for the argument area pointer… (authored by dcjm).
Fix for 32-in-64 on Unix. We can't use mlArg2Reg for the argument area pointer…
Mon, Oct 19, 12:36 PM
dcjm committed rPOLYMLa63dd183a786: Convert PolyObject * in first argument to FirstArgument type. This was missed… (authored by dcjm).
Convert PolyObject * in first argument to FirstArgument type. This was missed…
Mon, Oct 19, 12:36 PM
dcjm committed rPOLYML471fd261f2fc: Merge branch 'master' into CompileForeignCall (authored by dcjm).
Merge branch 'master' into CompileForeignCall
Mon, Oct 19, 12:36 PM
dcjm committed rPOLYML42a85daa50de: Tidy up and simplify the Windows GUI console. (authored by dcjm).
Tidy up and simplify the Windows GUI console.
Mon, Oct 19, 12:36 PM
dcjm committed rPOLYMLdd93dd4bb8a3: Fix return register in X86/64. Turn off debugging output. (authored by dcjm).
Fix return register in X86/64. Turn off debugging output.
Mon, Oct 19, 12:36 PM
dcjm committed rPOLYML060905df6845: Revert to using Edit control rather than RichEdit. (authored by dcjm).
Revert to using Edit control rather than RichEdit.
Mon, Oct 19, 12:36 PM
dcjm committed rPOLYMLec6bf52e2cd6: Modify old Foreign structure to take account of changes made in OS. (authored by dcjm).
Modify old Foreign structure to take account of changes made in OS.
Mon, Oct 19, 12:36 PM
dcjm committed rPOLYML6f37e47883ba: Merge branch 'PollChangesAgain' into CompileForeignCall (authored by dcjm).
Merge branch 'PollChangesAgain' into CompileForeignCall
Mon, Oct 19, 12:36 PM
dcjm committed rPOLYMLce39cdb5ff97: Rebuilt configure after merge. (authored by dcjm).
Rebuilt configure after merge.
Mon, Oct 19, 12:36 PM
dcjm committed rPOLYML0334be93fa3d: Merge branch 'master' into PollChangesAgain (authored by dcjm).
Merge branch 'master' into PollChangesAgain
Mon, Oct 19, 12:36 PM