On 29/11/2012, at 11:47 PM, Christian Sternagel wrote:
> On 11/09/2012 12:26 AM, Christian Sternagel wrote:
>> Just follow the "Browse theories" link of any devel entry, e.g.,
>> http://afp.sourceforge.net/browser_info/devel/HOL/Bondy/index.html
> As far as I can tell the problem still remains. I
On 11/29/2012 06:27 PM, Makarius wrote:
On Mon, 26 Nov 2012, Makarius wrote:
In the past few weeks, we've had isatest problems with
HOL-Quickcheck_Benchmark and ISABELLE_FULL_TEST=true (as used with
mac-poly64-M4 and mac-poly64-M8).
After some experimentation and tinkering, it seems that the
On 11/29/2012 10:22 PM, Makarius wrote:
On Thu, 29 Nov 2012, Makarius wrote:
I've also started some bisection about where the problem comes from,
without any clear results so far, but I will report more a bit later.
I've spent a few more hours on the problem, repeating the bisection
several
On Thu, 29 Nov 2012, Makarius wrote:
I've also started some bisection about where the problem comes from,
without any clear results so far, but I will report more a bit later.
I've spent a few more hours on the problem, repeating the bisection
several times, and staring add various changesets
On Mon, 26 Nov 2012, Makarius wrote:
In the past few weeks, we've had isatest problems with
HOL-Quickcheck_Benchmark and ISABELLE_FULL_TEST=true (as used with
mac-poly64-M4 and mac-poly64-M8).
After some experimentation and tinkering, it seems that the timeouts in
Isabelle/978200ae8473 from
On Thu, 29 Nov 2012, Lawrence Paulson wrote:
Will it run without compiled files? And will it run efficiently enough?
Certainly I've always compiled my copy.
On 21 Nov 2012, at 10:35, Makarius wrote:
* A version of Proof General as Isabelle component, like
http://isabelle.in.tum.de/compo
Will it run without compiled files? And will it run efficiently enough?
Certainly I've always compiled my copy.
Larry
On 21 Nov 2012, at 10:35, Makarius wrote:
> * A version of Proof General as Isabelle component, like
>http://isabelle.in.tum.de/components/ProofGeneral-4.1.tar.gz
>(it
On Thu, 29 Nov 2012, Makarius wrote:
The slight tendency away from Python APIs is another thing. Since
Isabelle/Scala is the official system programming language for quite some
time already, I've occasionally checked the situation for JVM-based access to
Mercurial operations. Projects like h
Hi all,
As you might already know, Daniel Kühlwein (a Ph.D. student of Josef Urban) and
I have been working on a machine-learning based relevance filter for
Sledgehammer, called MaSh. The idea is to learn from successful proofs which
facts are more likely to be useful for future proofs.
We are lo
On 11/09/2012 12:26 AM, Christian Sternagel wrote:
Just follow the "Browse theories" link of any devel entry, e.g.,
http://afp.sourceforge.net/browser_info/devel/HOL/Bondy/index.html
As far as I can tell the problem still remains. Is it known in the
meantime what the problem is?
cheers
chris
On Thu, 29 Nov 2012, Lars Noschinski wrote:
On 29.11.2012 12:13, Makarius wrote:
Does JGit work smoothly on Windows, for example? In Isabelle/Scala I
play more and more funny tricks to get rid of the received Unix model of
executing some process to do small auxiliary things.
I would expect so
On 29.11.2012 12:13, Makarius wrote:
Does JGit work smoothly on Windows, for example? In Isabelle/Scala I
play more and more funny tricks to get rid of the received Unix model of
executing some process to do small auxiliary things.
I would expect so: JGit is a pure Java implementation, not usin
On Thu, 29 Nov 2012, Lars Noschinski wrote:
The slight tendency away from Python APIs is another thing. Since
Isabelle/Scala is the official system programming language for quite
some time already, I've occasionally checked the situation for
JVM-based access to Mercurial operations. Projects l
On 29.11.2012 11:49, Makarius wrote:
For future changes it might be worth to keep in mind that the
Mercurial project considers the python interface as internal:
http://mercurial.selenic.com/wiki/MercurialApi
Right. This classification has somehow changed over the years. Back in
2008, use of th
On Thu, 29 Nov 2012, Lars Noschinski wrote:
I now wanted to suggest isabelle.in.tum.de as an obvious choice for a
gateway host, but it is not reachable via SSH from the outside =)
In ancient times isabelle.in.tum.de was indeed just an alias, say for
sunbroy60. So one had everything physicall
On Thu, 29 Nov 2012, Lars Noschinski wrote:
Since some time they also provide hosting of mercurial repositories.
This is what I meant by "home-made".
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informat
On Thu, 29 Nov 2012, Alexander Krauss wrote:
For future changes it might be worth to keep in mind that the Mercurial
project considers the python interface as internal:
http://mercurial.selenic.com/wiki/MercurialApi
Right. This classification has somehow changed over the years. Back in
2008
On 29.11.2012 11:28, Makarius wrote:
On Thu, 29 Nov 2012, Lars Noschinski wrote:
We could make up a rule "always go through host X" (X being one of the
macbroys/lxbroys) and hope it is the simultaneous access from multiple
hosts and not the fact that it is laying on a NFS which makes it
unreliab
On Thu, 29 Nov 2012, Lars Noschinski wrote:
So we still carry a lot of CVS baggage stemming from 1993, not just in
the low-level technological sense.
Nothing new, all known already. I usually ignore it to avoid the trouble
of thinking about more fundamental changes.
We could make up a rule "a
19 matches
Mail list logo
