Comments (3)
Unfortunately, using why3server -j $(nproc)
with gnatprove -j 1
does not sufficiently reduce the required memory.
Failing CI test: https://github.com/Componolit/RecordFlux/actions/runs/3621700551/jobs/6105479206
Used setup: https://github.com/Componolit/RecordFlux/blob/ba411ffdb2b6627125b245e3600442ed36f2d28c/Makefile#L180-L186
from recordflux.
With the current configuration, two gnatprove
processes are run in parallel. At most, two provers (due to why3server -j 2
) and two gnatwhy3
process (due to two parallel gnatprove -j 1
) are run in parallel.
I discussed the issue with @kanigsson. We see only two options:
- Try to reduce
--memlimit
to reduce the memory required bygnatwhy3
. - Only run one
gnatprove
instance (nowhy3server
needed).
from recordflux.
Reducing --memlimit
works. I will create a PR for allowing multiple parallel GNATprove processes. But I do not see an advantage in using a why3server
when running GNATprove with -j 1
, which restricts GNATprove to just use one gnatwhy3
or one prover in parallel, as parallelization is only achieved by multiple GNATprove processes. So I think it doesn't make sense to follow this route, as long as there is no possibility to limit the number of gnatwhy3
processes independently of the number of parallel provers.
from recordflux.
Related Issues (20)
- Enable DHCP client tests without Docker
- Add missing quotes to error message about invalid aspects HOT 1
- Style error leads to parser and model errors HOT 1
- Release 0.8.0 HOT 1
- Allow updating of generated files HOT 1
- Invalid "always true" error for enum with `Always_Valid` aspect HOT 1
- Release 0.9.0 HOT 1
- C code generator
- Refactoring of expressions HOT 4
- Problems trying to specify HDLC HOT 1
- Allow setting the GNATCOLL_ICONV_OPT environment variable when installing RecordFlux HOT 1
- Mathematical expression for first and last of integer types does not support parentheses to ensure the order of operations HOT 2
- Bug when including a condition on a field that is a message type HOT 4
- Allow setting the GNATCOLL_ICONV_OPT environment variable in Makefile HOT 9
- Very long build times for anything besides a trivial specification HOT 21
- Bug when comparing opaque values HOT 2
- Command line switch `rflx --no-verification --unsafe generate` doesn't seem to work HOT 3
- Missing `alr build` step either in instructions or in Makefile HOT 3
- `KeyError: 'data'` converting IANA Constrained RESTful Environments (CoRE) Parameters HOT 4
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from recordflux.