Hi Makarius,
This might be due to my attempt to repair Predicate_Compile_Examples in 78ece168f5b5. I'll
see what I can do.
Andreas
On 15/09/15 16:41, Makarius wrote:
This is the situation in Isabelle/0b071f72f330 and AFP/3085eb9e2bb9:
*** Failed to load theory "Execute_Main" (unresolved
It should work now again (Isabelle/e4716b792713 and AFP/ec3887abf158).
Sorry for the trouble,
Andreas
On 15/09/15 16:41, Makarius wrote:
This is the situation in Isabelle/0b071f72f330 and AFP/3085eb9e2bb9:
*** Failed to load theory "Execute_Main" (unresolved "Java2Jinja")
*** Failed to load
This is the situation in Isabelle/0b071f72f330 and AFP/3085eb9e2bb9:
*** Failed to load theory "Execute_Main" (unresolved "Java2Jinja")
*** Failed to load theory "JinjaThreads" (unresolved "Execute_Main")
*** Dependency "member_i_i" -> "case_list" would result in module dependency
cycle
*** At
Sorry was my mistake, should be fixed with d5a3dbc9da17 now.
- Johannes
Am Sonntag, den 16.11.2014, 19:48 +0100 schrieb Florian Haftmann:
isabelle: 059ba950a657 tip
afp: 0fdf8f639bb4 tip
Running JinjaThreads ...
JinjaThreads FAILED
(see also
isabelle: 059ba950a657 tip
afp: 0fdf8f639bb4 tip
Running JinjaThreads ...
JinjaThreads FAILED
(see also
/mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.2_x86-linux/log/JinjaThreads)
*** At command inductive (line 413 of
See now http://isabelle.in.tum.de/repos/isabelle/rev/47c8475e7864.
Interesting to see how bad dynamic typing actually is…
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP
Hi Stefan,
while doing a testall on the AFP, I noticed that JinjaThreads no longer
compiles. I get the error
*** exception Match raised (line 146)
***
*** At command ML (line 145 of
/mnt/home/berghofe/isabelle/afp/thys/JinjaThreads/Examples/BufferExample.thy)
This should be now fixed in
On Thu, 2 Feb 2012, Peter Lammich wrote:
... at least the superscripts of TOC and chapters, in the release-branch
of AFP.
Looks like it was built on a french latex configuration.
It is not there on the current tip, which is AFP/9235eceb731f. (It is
standard practice to specify repository
On 18/02/2012, at 1:35 AM, Makarius wrote:
On Thu, 2 Feb 2012, Peter Lammich wrote:
... at least the superscripts of TOC and chapters, in the release-branch
of AFP.
Looks like it was built on a french latex configuration.
It is not there on the current tip, which is AFP/9235eceb731f.
... at least the superscripts of TOC and chapters, in the release-branch
of AFP.
Looks like it was built on a french latex configuration.
Cheers,
Peter
___
isabelle-dev mailing list
isabelle-...@in.tum.de
Awesome :-)
Actually, I think it does what it is supposed to do. The document/root.tex says
\usepackage[french,english]{babel}
To me that reads like the primary language should be French (I might be wrong).
The difference is probably that the machine it was built on has more french
latex
On Fri, 13 Jan 2012, Makarius wrote:
But there is another problem with JinjaThreads right now:
Isabelle/d43ddad41d81
AFP/3dcc6b9eae2b
thys/JinjaThreads/Framework/FWDeadlock.thy line 251:
blast does not terminate and fills up memory
It looks like another set vs. pred thing stemming from
On Thu, 12 Jan 2012, Lukas Bulwahn wrote:
On 01/11/2012 09:29 PM, Alexander Krauss wrote:
The real problem is in fact JinjaThreads. AFAIK, the only machine at
TUM where it can still build (in principle) is lxbroy10, but as Lukas
pointed out there are still some failures, cf.
On 01/13/2012 06:24 PM, Makarius wrote:
I haven't been aware of that. The configuration goes back to myself, in
private communication with Alex. I did not check it later. In
4a892432e8f1 it is now more conventional, also tested manually to some
extend.
4a892432e8f1 merely modifies the setup
Hi all,
it seems indeed that JinjaThreads since recently runs out of memory even
on macbroy2 with parallelism, c.f. last afp isatest log:
Running HOL-Word-JinjaThreads ...
poly(19058,0xa00a0540) malloc: *** mmap(size=16777216) failed (error code=12)
*** error: can't allocate region
*** set a
JinjaThreads doesn't seem to run out of the box (on macbroy2, with
Poly/ML 5.3.0). It seems to run out of memory.
I use ML_OPTIONS=-H 500, but I would assume the AFP sets this appropriately.
Probably this is a known issue, but I don't know where to check for
the automatic AFP logs.
Clemens Ballarin wrote:
JinjaThreads doesn't seem to run out of the box (on macbroy2, with
Poly/ML 5.3.0). It seems to run out of memory.
I use ML_OPTIONS=-H 500, but I would assume the AFP sets this
appropriately.
Probably this is a known issue, but I don't know where to check for the
On 19/12/2010, at 8:16 AM, Alexander Krauss wrote:
Clemens Ballarin wrote:
JinjaThreads doesn't seem to run out of the box (on macbroy2, with Poly/ML
5.3.0). It seems to run out of memory.
I use ML_OPTIONS=-H 500, but I would assume the AFP sets this
appropriately.
Probably this is a
18 matches
Mail list logo
