PolyML.pretty and PolyML.context are eqtypes based on their current…

Check arity of constructors in where type before trying to apply realisation.

clarified signature;

tuned signature;

clarified command-line, following other build_XYZ tools;

merged

trying to streamline a few proofs

feat(sitegen-devel): switched to python3

renamings to ensure consistency with paper description

more recent OCaml and GHC stack: better support for Apple Silicon;

regen website

Merged

Monad_Memo_DP: curry opt_bst and slight tuning

Fix type-dependent functions, e.g. PolyML.print, if they were in a structure…

Fix indexing of vectors and arrays for PackReal32 on 64-bits.

clarified check of root process on Windows (NB: the winpid is less stable than…

merged

avoid "exec" to change the winpid;

fast approximation of test for process group (NB: initial process might already…

clarified signature;

rebuild executable for x86_64-darwin;

clarified command-line;

tuned comments;

update Linux base-line;

tuned signature;

simplified typesetting of \<guillemotleft>...\<guillemotright>;

collecting more lemmas concerning multisets

collecting more lemmas concerning multisets

proper use of antiquotations;

more realistic timeout;

tuned whitespace;

Tweaks

more documentation on "Conversions";

adapted to Isabelle/a2c589d5e1e4;

Merge

tweak

simplified proof

tuned

sshiftr/bl lemmas by Florian Märkl

proof simplification

Merge remote-tracking branch 'remotes/origin/master' into ARM64Testing

When loading code containing an FFI callback update the global heap base…

Use a writable address when setting data in the new constant area.

malloc and free are in stdlib.h on OpenBSD.

Only include ARM64 relocations if we're building for ARM64. The defines may not…

Some fixes for Unix.

Reorganise OS memory allocators.

Merge branch 'SeparateCodeAndConsts' into ARM64Merge

Update a relative address constant if it has moved even if it goes to the same…

Implement callbacks (FFI closures) in ARM64. There is still a problem with…

Merge branch 'AllocateInContiguous' into SeparateCodeAndConsts

Remove no_pie option for Mac OS. We're now generating position-independent…

Add a cast to quieten warning.

Add the name of the entry point to the Fail exception packet.

Fix matching in allocator.

Comment about displaying constant areas.

Only try with MAP_JIT trying to allocate fails without it. Earlier versions

Implement relocation for the address of the constants relative to the code.

Implement splitting of the constant area from code for ARM64. This is…

Implement relocations for ARM64 on Mac OS. Two small fixes for 32-in-64.

Fix ARM64 ADRP/LDR relocations for PECOFF.

Add space for UDF instruction. Don't scan code when interpreting.

Merge branch 'SeparateCodeAndConsts' into ARM64Merge

Add a no-op after references to the constant area to allow for patching and put…

Handle all cases in the switch rather than setting the value beforehand.

When splitting constants from code put them into the code area so they are…

Move GetConstSegmentForCode and related functions in MachineDependent.

Remove default heap size from bootstrap build.

Fix ELF and MachO exporters for change to ScanConstant.

Fix problem with relative addresses that had not been updated.

Merge branch 'AllocateInContiguous' into SeparateCodeAndConsts

Fix share-common-data. Code that is only reachable by a relative call or jump…

Fix for pecoff after recent changes. Add assertions. This seems to be broken…

Change ScanConstant and GetConstantValue to take the displacement of the code…

Use 32-bit relative jumps/calls in native 64-bit mode where possible.

In native X86/64 put all new code in a single 2GB area. This means that 32-bit…

Fix to Unix version after testing.

Merge branch 'BootFromInterpreter' into SeparateCodeAndConsts

Split the memory allocators for the native and 32-in-64 bit versions so both…

Fix the problem with restoring length words of code areas when the constant…

Move the fudge subtraction of 4 with relative offsets so that it applies to…

Some fixes for when the executable area is not writable.

When exporting an object file on X86/64 separate the constants from the code.

Fix work-around when it's not needed.

Work around for apparent bug in Mac OS. Reading directly into

#undef WORDS_BIGENDIAN in the Windows config.h since it's always little-endian.

Use the autoconf endian macro rather than trying to work out the endianness.

Use MAP_JIT on the initial mmap but then use mprotect to create the pages in 32…

Rebuild config files after change to configure.ac.

Mac OS fixes, primarily to do with write access to executable memory.

MacOS reports the host as "arm" not "arm64". Add detection for…

Avoid warnings with anonymous semaphores in MacOS.

Missed one item in previous commit.

Fix cache clear in Mac OS. Add underscores to assembly code functions if…

Add ARM64 to mach-o export.

Don't try sem_init and sem_destroy on Mac OS X, they're deprecated.

Only check range of int and unsigned if necessary.

Use SBFX for LargeWord.fromInt in 32-in-64. This untags and sign-extends in a…

Fix length field in allocation in RTS calls.

Fix scaling for C loads/stores. Restore Real32 operations that had been…