proper support for Windows exe;

proper Isabelle component settings: prefer standard terminology…

provide verit-2020.10-rmx for testing (inactive);

proper setup for Windows/MinGW;

proper libraries_closure for libgmp;

tuned;

updated to polyml-test-d68c6736402e --- follow current ongoing development;

localized example to avoid name clashes

tuned names

The general "tail" instruction is now in the extended set.

merged

tuned names

Fix offsets in test.

genRTSCallFastGeneraltoFloat is now an extended operation.

LoadC8/StoreC8 use genCAddress so that involves an extra item on the stack.

LoadC8/StoreC8 now take both an offset and an index as with the other C-memory…

Don't build the UnixSock structure on Windows.

update build script for veriT 2020.10-rmx

merged

more robust;

proper target directory for libraries;

proper library names on Windows;

build Isabelle Zipperposition component from OPAM repository;

proper support for Windows/Cygwin: "zipperposition" vs. "zipperposition.exe";

tuned messages --- less SPAM;

tuned;

tuned signature;

misc tuning and clarification: prefer Executable.libraries_closure;

tuned;

more portable;

reconstruction of veriT proofs in NEWS

Revert accidental inclusion of project file in last commit.

Fix K and E exports for 32-in-64.

PE/COFF exporter: Save the first relocation and write it to the end of the…

Move one opcode value because the value was still being used during the…

Remove the intermediate stage instructions and add a couple of reduced…

Combine jump with equalLocalB.

Combine the tag check instructions with jumps.

Move some more rarely used instructions into the escaped instruction group.

Replace a conditional branch round an unconditional branch by a conditional…

Link branches together to avoid a branch to a branch.

Add an optimisation pass. Currently this only deals with eliminating…

Add some combined instructions that implement common sequences for datatype tag…

Improvements to interpreted code and the interpreter. Add code to handle…

Fix bug that only showed up after several bootstraps.

Fix bug in indexed case in the interpreter. Start adding composite…

Overhaul the interpreted code. Separate rarely used instructions into two-byte…

Add separate descriptors for entry points and weak references. These are…

Merge branch 'master' of https://github.com/dcjm/polyml

Add hint file for Visual Studio.

Change DEBUGGER signature in ROOT file for interpreted version

add reconstruction for the SMT solver veriT

Add well-foundedness of trivial unit relation

NEWS;

activate E 2.5 for production use (see also 5d1a7b688f6d);

clarified signature;

clarified Executable.libraries_closure;

dedicated module for toplevel target handling

consolidated names and operations

replaced combinators by more conventional nesting pattern

avoid _cmd suffix where no Isar command is involved

centralized case distinction for beginning and ending nested targets in one…

adjusted to changes in distribution

replaced combinators by more conventional nesting pattern

consolidated names and operations

support for platform-specific executables;

removal of a synonym

merged

merged

tidying and removal of legacy name

tuned whitespace;

more robust: ignore existing gmp installation, but let veriT incorporate…

presumably redundant (absent in Windows/Cygwin download);

clarified signature;

tuned messages;

build Isabelle veriT component from official download;

tuned;

tuned messages;

direct exit to theory when ending nested target on theory target

tuned

consolidated terminology

avoid baroque export

clarified message;

tuned signature;

clarified options;

clarified signature: allow complex bash script;

more explicit MinGW context;

more standard path output (despite platform_path from d55eb82ae77b);

clarified signature;

clarified errors;

tuned signature;

more explicit MinGW context;

more libs for build_csdp;

support for MSYS2/MinGW64 on Windows;

tuned --- according to instructions on Website;

updated to csdp-6.1.1, with support for arm64-linux;

proper support for x86_64-windows via msys/mingw64;

more standard build from sources;

tuned message;

component csdp-6.2.0 for testing: example #2 in theory HOL-ex.SOS fails with…