Merge branch 'ARM64Development' into ARM64Testing

Remove fallback to interpreter from RTS and foreign call. It's no longer…

Implement loads from C memory.

Merge branch 'ARM64Development' into ARM64Testing

Implement allocation and freeing of memory on the C stack.

Merge branch 'ARM64Development' into ARM64Testing

Implement floating point comparisons. Check overflow on floating-point to int…

Implement real and float arguments and results for RTS calls.

Convert int directly to Real32.real rather than via Real.real. Implement…

Remove explicit rounding mode from DoubleToFloat built-in and use the current…

Implement floating point operations: add, subtract, multiply and divide for…

Implement atomic operations for mutexes.

Implement large word operations.

Remove compilerDebug switch control so that the ARM64 code-generator is always…

Implement fixed precision quot and rem and hence div and mod. Fix bug in range…

Implement the arbitrary precision operations just by calling the long-precision…

Implement fixed precision integer multiplication. Extend the bit field and…

Implement block word move.

Distinguish more precisely between the cases where 31 refers to SP and XZR.

Implement mutually-recursive closures.

Implement block byte ordered comparison.

Implement addresses with index and non-zero offset.

Implement byte block move.

Implement allocation of vectors and arrays. Fix stack arguments in tail…

Implement storeMLByte, storeUntagged and clearMutable. Fix length in variable…

Implement byte-vector equality, primarily used for strings. Fix Word.mod which…

Implement allocation of byte vectors and strings.

Merge branch 'master' into ARM64Development

Implement RTS calls with non-floating point arguments and result.

Add infrastructure for RTS calls and FFI calls/callbacks.

Add test-bit-and-branch and compare-and-branch instructions.

Implement word shifts.

Implement multiply, div and mod on word.

Implement indexed case.

Fix moving arguments when calling the interpreter.

Implement word logical operations.

Implement check-rts-exception.

Implement exception handlers.

Handle the case of interpreted code raising an exception with a native code…

Implement move-to-container.

Move the construction of the instruction list into the upper level of the code…

Avoid pushing and popping arguments to unary and binary built-ins.

Implemented load-byte and load-word with indexing and set-stack-value, used in…

Add a general function for addition/subtraction of constants.

Use X0 to hold the top of the stack where possible. This avoids a lot of…

Fix stack check limit.

Implement addition and subtraction for fixed precision int and word. Implement…

Implement "not" and get-thread-index.

Add various instructions to the low-level so they can be used by the code…

Add logical operations with constants, shifts and byte loads and stores.

Return a SysWord.word value when trying to create a CIF if libffi is not…

Print the unimplemented interpreter instructions that force fallback.

Add functions to encode and decode bit pattern constants used in AND, OR and…

Implement test of tag bit. Fix bug in closure construction. Work around…

Implement memory allocation for tupling and closures.

Implement comparisons.

cosmetic tweaks to proofs

updated example;

clarified options (again);

more options: update ISABELLE_IDENTIFIER;

clarified conditional ML;

support for conditional ML text;

updated example;

clarified options;

Reinstate tests on the command argument to Unix.execute to check it is…

Implement Unix.executeInEnv and hence Unix.execute largely in C rather

Update the Windows library code for the FFI changes.

proper context variable handling when stripping leadings quantifiers from test…

merged

minor stylistic changes

Add completeness of modal logics T, KB, K4, S4 and S5

Stylistic tweaks, which I hope are improvements :-)

proper etc/ISABELLE_ID from archive (amending 4cba4e250c28);

eliminated perl: prefer elementary GNU printenv;

more self-contained support for macOS;

more robust bootstrap of components;

misc tuning and clarification;

tuned signature;

updated paper references

support for base64 via Isabelle/Scala/ML;

compile;

clarified signature (again);

clarified signature: avoid overlap of String vs. Bytes (both are CharSequence);

merged

clarified signature;

clarified signature: more structured arguments, notably for remote provers;

unused;

clarified signature;

unused;

clarified message output: flush already happens in write_message_yxml (see…

clarified signature for Scala functions;

clarified signature: avoid tmp file;

tuned;

clarified cache;

clarified exceptions;

clarified signature: Bytes extends CharSequence already (see d201996f72a8);

more uniform use of Byte_Message;

tuned signature;

tuned signature;

more robust treatment of empty markup: it allows to produce formal chunks;