Thanks to a steve_j_wright post (http://sourceforge.net/forum/forum.php?thread_id=1963966&forum_id=373711)
I change the way rodin launches :
"C:\Program Files\rodin 0.8.1\rodin.exe" -vm java.exe -vmargs -Xms600m -Xmx800m instead of
"C:\Program Files\rodin 0.8.1\rodin.exe"
(I have only a 1 GB for RAM and i will have to change the PC for enlarging RAM from now on !)
Then the problem stops ! ;-)
But the next refinements will probably remind me that problem...
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
The root of the problem is memory usage. The marker reported is due to an OutOfMemory exception while auto-proving the machine.
The large memory consumption is due to the format in which proofs are stored in the database. The current format is too detailed for proper handling of a large set of POs. We currently have a six-fold increase between the PR file size and the core memory used to represent it. For instance, a PR file of 27 Mb uses 165 Mb of heap space.
Another direction is to prune the forward inferences which are present but unused in a proof. Here, there are a lot of axioms which are not normalized and produce forward inferences for normalizing them, although these axioms are seldom relevant to the proof at hand. Such pruning of unused forward steps would be a giant step towards smaller proof files.
Changed the nature of this entry to "feature request".
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
If you modify the context, so that all predicates "x ≠ y" are rewritten as "¬x = y" (see attached file), then the auto-prover can be run in less than 64 Mb. The resulting PR file is about 1.2 Mb. I consider this acceptable.
Consequently, the UI must be changed so that it generates normalized predicates for enumerated sets (see FR #1949585). A complement approach would be to trim down proofs when committing them, by removing useless forward rules (see FR#1949582).
File Added: c00.buc
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
project example
Logged In: NO
Thanks to a steve_j_wright post (http://sourceforge.net/forum/forum.php?thread_id=1963966&forum_id=373711)
I change the way rodin launches :
"C:\Program Files\rodin 0.8.1\rodin.exe" -vm java.exe -vmargs -Xms600m -Xmx800m instead of
"C:\Program Files\rodin 0.8.1\rodin.exe"
(I have only a 1 GB for RAM and i will have to change the PC for enlarging RAM from now on !)
Then the problem stops ! ;-)
But the next refinements will probably remind me that problem...
Logged In: YES
user_id=1041912
Originator: NO
The machine produces 348 proof obligations. The PR file grows very large: e.g., 24 Mb for 112 discharged POs.
The cause of the large PR file is the extensive use of forward rules and/or of ML.
Need to see what can be done to make the file smaller.
Logged In: YES
user_id=1041912
Originator: NO
The root of the problem is memory usage. The marker reported is due to an OutOfMemory exception while auto-proving the machine.
The large memory consumption is due to the format in which proofs are stored in the database. The current format is too detailed for proper handling of a large set of POs. We currently have a six-fold increase between the PR file size and the core memory used to represent it. For instance, a PR file of 27 Mb uses 165 Mb of heap space.
Another direction is to prune the forward inferences which are present but unused in a proof. Here, there are a lot of axioms which are not normalized and produce forward inferences for normalizing them, although these axioms are seldom relevant to the proof at hand. Such pruning of unused forward steps would be a giant step towards smaller proof files.
Changed the nature of this entry to "feature request".
Context with normalized predicates
Logged In: YES
user_id=1041912
Originator: NO
If you modify the context, so that all predicates "x ≠ y" are rewritten as "¬x = y" (see attached file), then the auto-prover can be run in less than 64 Mb. The resulting PR file is about 1.2 Mb. I consider this acceptable.
Consequently, the UI must be changed so that it generates normalized predicates for enumerated sets (see FR #1949585). A complement approach would be to trim down proofs when committing them, by removing useless forward rules (see FR#1949582).
File Added: c00.buc