vprover / vampire

The Vampire Theorem Prover
https://vprover.github.io/
Other
297 stars 52 forks source link

Reduce reliance on platform-specific APIs, improve Windows support #462

Open MichaelRawson opened 1 year ago

MichaelRawson commented 1 year ago

Vampire should not need a great deal of platform-specific code. This is a tracking issue to remove as much as possible, and make what we absolutely need as cross-platform as we can.

We currently use platform-specific code:

I'm currently looking at whether we can remove the memory allocator and the semaphores. Watch this space!

MichaelRawson commented 1 year ago

Using something akin to UNIX fork() is not really negotiable - we want to keep the existing Vampire state, notably the parsed problem, when we start a strategy - but it doesn't exist on Windows. We will have to rely on Cygwin for this on Windows, and hope that the various incompatibilities don't bite us.

MichaelRawson commented 1 year ago

Allocator is dead, long live Allocator! #469 removed the platform-specific code for allocation.

MichaelRawson commented 6 months ago

No more semaphores, no more semaphore support requirement.

MichaelRawson commented 1 month ago

Replacing global operator new portably to limit memory usage was so painful in the end (#592) that we gave up and call POSIX setrlimit in #594. Ho hum. Better POSIX than Linux.