Hi Johannes,
> I tried to reduce the runtime requirement of HOL-Probability by removing
> some of the sublocale instantiations. As a lot of time is spend in
> locale interpretation inside proofs.
Is the same interpretation repeated over and over? In that case the
corresponding proposition can be
On Tue, 20 Sep 2011, Makarius wrote:
In the meantime I have investigated this a little bit. It seems that
HOL-Probability requires quite some memory even in minimalistic batch mode --
approx. 2GB on my 4GB machine. With Isabelle/jEdit one needs further 600 MB
for the editor process and the sa
On Tue, 13 Sep 2011, Lars Noschinski wrote:
. Reduced CPU performance requirements, usable on machines with few
cores.
. Reduced memory requirements due to pruning of unused document
versions (garbage collection).
As some data point: I was able to load HOL/Probability/Probability.thy
(using
On 18.09.2011 17:05, Makarius wrote:
On Tue, 13 Sep 2011, Lars Noschinski wrote:
I was irritated when Isabelle/jEdit complained about missing theory
files, when the files where obviously there (and loaded). Later I
found out, that this error is also displayed if there are any errors
(transitivel
On Tue, 13 Sep 2011, Lars Noschinski wrote:
Is Isabelle/jEdit supposed to work with Pure as a logic image? On
one occasion, it misparsed a document because it did not consider
datatype as a keyword.
Yes, but it is a bit difficult to load a session from there that defines
many commands, like m
On Tue, 13 Sep 2011, Lars Noschinski wrote:
I was irritated when Isabelle/jEdit complained about missing theory
files, when the files where obviously there (and loaded). Later I found
out, that this error is also displayed if there are any errors
(transitively) in these theory files.
Did you
On 13.09.2011 12:01, Walther Neuper wrote:
On 09/13/2011 11:38 AM, Lars Noschinski wrote:
- The command line help shows some option "-l" to use a different
logic image, but this does not seem to work.
"-l" works perfectly for us: for instance,
/usr/local/isabelle/bin/isabelle jedit -l Isac Tes
On 09/13/2011 11:38 AM, Lars Noschinski wrote:
- The command line help shows some option "-l" to use a different
logic image, but this does not seem to work.
"-l" works perfectly for us: for instance,
/usr/local/isabelle/bin/isabelle jedit -l Isac Test_Isac.thy &
runs all tes
On 06.09.2011 21:58, Makarius wrote:
* Improved Isabelle/jEdit Prover IDE (PIDE), which can be invoked as
"isabelle jedit" on the command line.
. Management of multiple theory files directly from the editor
buffer store -- bypassing the file-system (no requirement to save
files for checking).
On Tue, 6 Sep 2011, Makarius wrote:
* Improved Isabelle/jEdit Prover IDE (PIDE), which can be invoked as
"isabelle jedit" on the command line.
The required build component is still the same:
http://www4.in.tum.de/~wenzelm/test/jedit_build-20110622.tar.gz
Makarius
__
* Improved Isabelle/jEdit Prover IDE (PIDE), which can be invoked as
"isabelle jedit" on the command line.
. Management of multiple theory files directly from the editor
buffer store -- bypassing the file-system (no requirement to save
files for checking).
. Markup of formal entities
11 matches
Mail list logo
