Re: [isabelle-dev] AFP devel broken
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. Is it known in the meantime > what the problem is? Not really. It now overlaps less with isatest, but the log still mostly ends in the middle of HOL-Probability (e.g. see below). It appears those processes all just get stuck and sit there. I've moved the afp test 2h later to eliminate any overlap with isatest, but that's probably not it. I have some more ideas what to look at, but was away last week and at SSV'12 this week. Next week is looking better for progress on this. Cheers, Gerwin Start test for /home/isatest/afp/devel at Thu Nov 29 06:30:56 CET 2012, macbroy2 begin hg pull/update pulling from ssh://isat...@afp.hg.sourceforge.net/hgroot/afp/afp searching for changes adding changesets adding manifests adding file changes added 2 changesets with 42 changes to 42 files 42 files updated, 0 files merged, 0 files removed, 0 files unresolved remote: Running preoutgoing hook remote: Use of uninitialized value in concatenation (.) or string at /etc/mercurial/preoutgoing line 36. end hg pull/update AFP version: development -- hg id 40ecbad14077 Isabelle version: devel -- hg id 902f2efa Building HOLCF ... Finished HOLCF (0:00:43 elapsed time, 0:01:10 cpu time, factor 1.62) Building HOL-Nominal ... Finished HOL-Nominal (0:00:15 elapsed time, 0:00:25 cpu time, factor 1.66) Building HOL-Multivariate_Analysis ... Finished HOL-Multivariate_Analysis (0:02:21 elapsed time, 0:06:46 cpu time, factor 2.87) Building HOL-Word ... Finished HOL-Word (0:00:33 elapsed time, 0:01:16 cpu time, factor 2.30) Building Jinja ... Finished Jinja (0:04:44 elapsed time, 0:14:27 cpu time, factor 3.05) Building LatticeProperties ... Finished LatticeProperties (0:00:16 elapsed time, 0:00:24 cpu time, factor 1.50) Building HOL-Probability ... The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL-Quickcheck_Benchmark timeouts
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 timeouts in Isabelle/978200ae8473 from last Friday work: we've had successful isatest runs over the weekend. As far as I can see, the tests on macbroy2 terminate around 05:30 CET. This might be relavant for later tests of AFP. That was too optimistic. It seems that find_unused_assms uses a lot of stack space, and thus fills up memory on x86_64. I've addressed this in f25bcb8a4591 to get more explicit failure. 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. Is Lukas Bulwahn still looking after his stuff, or is this now unmaintained? It must be considered unmaintained. The benchmarks themself I will irregularly have time on weekends and nights to have a look, but I cannot keep up with "Isabelle roaring ahead". Lukas Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL-Quickcheck_Benchmark timeouts
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 times, and staring add various changesets that are not at all
clear from their text.
This is the result:
50e457bbc5fe bulwahn GOOD
6a26fed71755 bulwahn SKIP (BAD)
28cd3c9ca278 bulwahn SKIP (BAD)
fb696ff1f086 bulwahn BAD
Due to skipped revisions, the first bad revision could be any of:
changeset: 49943:6a26fed71755
user:bulwahn
date:Sat Oct 20 09:09:32 2012 +0200
summary: passing names and types of all bounds around in the simproc
changeset: 49944:28cd3c9ca278
user:bulwahn
date:Sat Oct 20 09:09:33 2012 +0200
summary: tuned tactic in set_comprehension_pointfree simproc to
handle composition of negation and vimage
changeset: 49945:fb696ff1f086
user:bulwahn
date:Sat Oct 20 09:09:34 2012 +0200
summary: adjusting proofs
And here some explanation reconstructed from the investigations with
some guesswork, glossing over the the unexplained things in these
changesets.
(1) BAD means the following crash:
theory A imports Main
begin
find_unused_assms Fun
Warning - Unable to increase stack - interrupting thread
Exception trace for exception - Interrupt
Generated_Code.value(1)(1)(1)(1)(2)
Generated_Code.check_all_subsets(4)(1)
Exhaustive_Generators.compile_generator_expr(2)compile-(1)(1)(1)(1)(1)
Exhaustive_Generators.compile_generator_expr(2)(1)(1)
Quickcheck_Common.test_term_with_cardinality(5)test_card_size(4)
Quickcheck_Common.test_term_with_cardinality(5)test(2)
Quickcheck_Common.test_term_with_cardinality(5)
Quickcheck_Common.generator_test_goal_terms(5)
(2) SKIP means these changesets were broken: HOL did not compile.
Backporting the "adjusting proofs" changeset fb696ff1f086, revealed
that they were BAD, too.
Note that it does not make any sense to publish changesets where Pure
or HOL do not compile. There is no obligation to have all session OK
all the time before pushing, but the usefulness of changesets is
greatly diminished. Someone else needs to spend much more time in
exchange for the 2-3 minutes saved in not running HOL on the spot,
before saying "hg commit". (I usually do a full "isabelle build -a"
before *any* commit.) And of course, there is an obligation to run
full "isabelle build -a" (or a proven equivalent) before any push.
(3) Looking at the critical change 6a26fed71755 "passing names and
types of all bounds around in the simproc" several times, I tried to
understand why it affects the generated quickcheck code in such a bad
way. (The changelog merely repeats the diff in English prose as a
"parrot".)
So after backing-out this single-line change from 5a1194acbecd of
today, everything worked fine except for
src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy crashing as follows:
*** Wellsortedness error
*** (in code equation Set_Comprehension_Pointfree_Tests.union ?a ?b ==
{x. x : ?a | x : ?b}):
*** Type nat not of sort enum
*** No type arity nat :: enum
*** At command "export_code" (line 134 of
"~~/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy")
Looking in the vicinity of the many other changes related to the
critical three above reveals the following:
changeset: 49947:29cd291bfea6
user:bulwahn
date:Sat Oct 20 09:09:37 2012 +0200
files: src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy
description:
adding another test case for the set_comprehension_simproc to the
theory in HOL/ex
So here one could guess from the greater context that 6a26fed71755
with its SKIP (BAD) status was motivated by a problem with passing
sort information down to the generated code. Since this is the
"exhaustive" quickcheck tester, having "nat :: enum" or not could make
a difference in the amount of enumeration done here.
So "BAD" might actually mean "better" in the sense of more exhaustive,
but it breaks down the concrete application of find_unused_assms
nonetheless.
Another side remark: Isabelle does not have a tradition for "test
cases" and "unit tests". What we usually made in all these decades
were some half-decent applications to explore tools or some stylized
examples to show the main points. These then also serve as a tests
somehow. (There is sometimes the odd situation that some manual or
"test" theory is the only spot where certain features of certain tools
occur, which means there is lack of proof for practical relevance.
I've seen this again just today in a different situation that is
unrelated to this incident.)
Anyway, maybe Lukas himself or codegen export Florian knows how to
resolve the situation.
I could have time on the weekend to have a closer look again.
The time when these changesets were pushed was rather bad, as at that
time you were on
Re: [isabelle-dev] HOL-Quickcheck_Benchmark timeouts
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 that are not at all
clear from their text.
This is the result:
50e457bbc5fe bulwahn GOOD
6a26fed71755 bulwahn SKIP (BAD)
28cd3c9ca278 bulwahn SKIP (BAD)
fb696ff1f086 bulwahn BAD
Due to skipped revisions, the first bad revision could be any of:
changeset: 49943:6a26fed71755
user:bulwahn
date:Sat Oct 20 09:09:32 2012 +0200
summary: passing names and types of all bounds around in the simproc
changeset: 49944:28cd3c9ca278
user:bulwahn
date:Sat Oct 20 09:09:33 2012 +0200
summary: tuned tactic in set_comprehension_pointfree simproc to handle
composition of negation and vimage
changeset: 49945:fb696ff1f086
user:bulwahn
date:Sat Oct 20 09:09:34 2012 +0200
summary: adjusting proofs
And here some explanation reconstructed from the investigations with some
guesswork, glossing over the the unexplained things in these changesets.
(1) BAD means the following crash:
theory A imports Main
begin
find_unused_assms Fun
Warning - Unable to increase stack - interrupting thread
Exception trace for exception - Interrupt
Generated_Code.value(1)(1)(1)(1)(2)
Generated_Code.check_all_subsets(4)(1)
Exhaustive_Generators.compile_generator_expr(2)compile-(1)(1)(1)(1)(1)
Exhaustive_Generators.compile_generator_expr(2)(1)(1)
Quickcheck_Common.test_term_with_cardinality(5)test_card_size(4)
Quickcheck_Common.test_term_with_cardinality(5)test(2)
Quickcheck_Common.test_term_with_cardinality(5)
Quickcheck_Common.generator_test_goal_terms(5)
(2) SKIP means these changesets were broken: HOL did not compile.
Backporting the "adjusting proofs" changeset fb696ff1f086, revealed that
they were BAD, too.
Note that it does not make any sense to publish changesets where Pure or
HOL do not compile. There is no obligation to have all session OK all the
time before pushing, but the usefulness of changesets is greatly
diminished. Someone else needs to spend much more time in exchange for
the 2-3 minutes saved in not running HOL on the spot, before saying "hg
commit". (I usually do a full "isabelle build -a" before *any* commit.)
And of course, there is an obligation to run full "isabelle build -a" (or
a proven equivalent) before any push.
(3) Looking at the critical change 6a26fed71755 "passing names and types
of all bounds around in the simproc" several times, I tried to understand
why it affects the generated quickcheck code in such a bad way. (The
changelog merely repeats the diff in English prose as a "parrot".)
So after backing-out this single-line change from 5a1194acbecd of today,
everything worked fine except for
src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy crashing as follows:
*** Wellsortedness error
*** (in code equation Set_Comprehension_Pointfree_Tests.union ?a ?b == {x. x :
?a | x : ?b}):
*** Type nat not of sort enum
*** No type arity nat :: enum
*** At command "export_code" (line 134 of
"~~/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy")
Looking in the vicinity of the many other changes related to the critical
three above reveals the following:
changeset: 49947:29cd291bfea6
user:bulwahn
date:Sat Oct 20 09:09:37 2012 +0200
files: src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy
description:
adding another test case for the set_comprehension_simproc to the theory
in HOL/ex
So here one could guess from the greater context that 6a26fed71755
with its SKIP (BAD) status was motivated by a problem with passing sort
information down to the generated code. Since this is the "exhaustive"
quickcheck tester, having "nat :: enum" or not could make a difference in
the amount of enumeration done here.
So "BAD" might actually mean "better" in the sense of more exhaustive, but
it breaks down the concrete application of find_unused_assms nonetheless.
Another side remark: Isabelle does not have a tradition for "test cases"
and "unit tests". What we usually made in all these decades were some
half-decent applications to explore tools or some stylized examples to
show the main points. These then also serve as a tests somehow. (There is
sometimes the odd situation that some manual or "test" theory is the only
spot where certain features of certain tools occur, which means there is
lack of proof for practical relevance. I've seen this again just today in
a different situation that is unrelated to this incident.)
Anyway, maybe Lukas himself or codegen export Florian knows how to resolve
the situation.
Once the HOL-Quickcheck-Benchmark session is up and running again, I would
like to apply some trivial changes to make it properly run in parallel.
Then it should become part of the normal build,
Re: [isabelle-dev] HOL-Quickcheck_Benchmark timeouts
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 last Friday work: we've had successful isatest runs over the weekend. As far as I can see, the tests on macbroy2 terminate around 05:30 CET. This might be relavant for later tests of AFP. That was too optimistic. It seems that find_unused_assms uses a lot of stack space, and thus fills up memory on x86_64. I've addressed this in f25bcb8a4591 to get more explicit failure. 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. Is Lukas Bulwahn still looking after his stuff, or is this now unmaintained? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the next release
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/components/ProofGeneral-4.1.tar.gz (it must be platform/emacs independent, without .elc files). As far as I remember, we've never had a bundled version of Proof General with compiled .elc files. These are non-portable across Emacs versions, so it will not work by default. Working a bit slower is better than not working at all. Once users start recompiling and rearranging things, it gets more like IKEA do-it-yourself software. (I am myself an expert of IKEA hardware assembly for the kitchen and usually enjoy it. Not for software, though.) BTW, for recompiling you need Unix "make", and that is not installed by default on any of the 3 platform families: Linux, Mac OS X, Windows. Generally, it touches the question if Proof General should be bundled at all. I started that a long time ago to approximate an out-of-the-box experience for Isabelle, but never succeeded in the last consequence. Right now there are PG 3.7.1.1, 4.0, 4.1 being activly used, so which one to chose? (I would have taken the latest stable version.) Coq never had a PG bundled either, and expert users expect it like that. David Aspinall never liked the bundling of Isabelle Proof General in the first place. So is it time to stop it? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the next release
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 must be platform/emacs independent, without .elc files). ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Reasons mira crashes
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 http://hg4j.com/ are not very far yet. Also interesting is http://mercurial.selenic.com/wiki/CommandServer which is a third way to the API vs. external executable problem: some hg process is started once and used with a certain protocol over the pipe. This project looks more relevant than hg4j, and it uses the CommandServer already: https://bitbucket.org/aragost/javahg/overview So it might become relevant for the Prover IDE some day. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Sledgehammer machine learning
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 looking for volunteers to try it out. By default, Sledgehammer uses the
good old MePo (Meng & Paulson) filter, but if you do either of the following,
you'll find yourself using a combination of MePo and MaSh:
1. sledgehammer_params [fact_filter = mesh] -- at the top of your theory
2. sledgehammer [fact_filter = mesh] -- for a single invocation
3. export MASH=yes
("mesh" = "mash" + "mepo"; yes, the names are a bit crazy. You can also cheat
and drop "fact_filter =".)
You will need a recent repository version (e.g. 05f8ec128e83) as well as Python
on your machine (which you probably already have).
The Sledgehammer manual has some documentation on MaSh. To get the latest
version:
isabelle build_doc Sledgehammer
isabelle doc sledgehammer
Sections 5.1, 6.1, and 7.2 are relevant. There's not much to know really -- the
learning and use of that learning takes place automatically (but can be guided
in various ways).
Example:
theory Scratch
imports Main
begin
lemma "map f xs = ys ==> rev (zip xs ys) = zip (rev xs) (rev ys)"
The command
sledgehammer learn_isar
forces learning at this point, so that we can start using MaSh right away.
(Otherwise, learning takes place in the background and is available only
from the second Sledgehammer invocation.) This takes about 5 seconds and prints
MaShing through 7127 facts for Isar proofs...
Learned 4644 nontrivial Isar proofs.
Next step:
sledgehammer [prover = e, fact_filter = mesh, verbose]
This prints
ATP: Including (up to) 1000 relevant facts:
zip_append list_induct2 ... divide_nonneg_pos wf_lenlex.
...
Facts in "e" proof (of 1000): zip_rev@4, length_map@11.
...
Try this: by (metis length_map zip_rev) (20 ms).
"@4" and "@11" indicate that the 4th and 11th facts are used for the proof. The
lower the numbers, the better. If we try again
sledgehammer [prover = e, fact_filter = mesh, verbose]
we get
Facts in "e" proof (of 1000): zip_rev@1, length_map@5.
which is an improvement that comes from learning. In contrast, MePo doesn't get
any smarter:
sledgehammer [prover = e, fact_filter = mepo, verbose]
Facts in "e" proof (of 1000): zip_rev@4, length_map@14.
The learning is persistent across sessions and should be robust in the face of
theory reorganizations etc.
If you want to improve MaSh's accuracy, you can let
sledgehammer learn_atp
run for hours with your favorite theories loaded. It will then invoke
Sledgehammer on each available theorem to learn from its proofs. You can
interrupt it any time. Learning from ATP proofs is usually better than learning
from human-written proofs, according to evaluations by Kühlwein, Urban et al.
I hope those of you who use Sledgehammer regularly will give this a try and let
me know about your experience. We've had very useful feedback about brand new
features this way before (e.g. the tight SPASS integration). If you have nice
examples, they might easily end up in one of our papers.
Cheers,
Jasmin
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] AFP devel broken
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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [OT] Reasons mira crashes
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: JGit is a pure Java implementation, not using C Git. But this is again a Git approach: public file formats. The Mercurial guys don't do that. This is getting more and more off-topic. And in fact, my main complaint about git is the noise and advocacy around it. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [OT] Reasons mira crashes
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 using C Git. You don't change such fundamental platforms without getting a real benefit from it. Of course. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [OT] Reasons mira crashes
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 like http://hg4j.com/ are not very far yet. JGit is said to be stable and full-featured. I know, and I still dislike the general style of Git and its tools. 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. Anyway, back then in 2008 we spent several months investigating the situation, and many week to prepare the move. In retrospect the choices were good ones. You don't change such fundamental platforms without getting a real benefit from it. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] [OT] Reasons mira crashes
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 the API was encouraged more. Switching to a CLI interface requires a bit of work, though. Just to recall the original motivations for using Mercurial instead of Git (which was not as aggressible marketed in 2008 as now so there was a genuine choice to be made): (1) Mercurial emphasizes a nice semantic model of monotonic history and immutable changes (in coincidence with the Isabelle/ML approach and the then emerging PIDE document model). This is true for the UI, for the underlying model Git is the pure one: If you do e.g. a rebase, mercurial makes a non-monotonic change to its storage, while Git preserves the old history, and only changes the branch pointer. 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 http://hg4j.com/ are not very far yet. JGit is said to be stable and full-featured. [But of course, changing our choice is not an option at this point.] -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Reasons mira crashes
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 physically on one fairly robust Sun server. Times have changed, and even the server-class machines are failing routinely now (lxbroy10). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Reasons mira crashes
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.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Reasons mira crashes
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, use of the API was encouraged more. Switching to a CLI interface requires a bit of work, though. Just to recall the original motivations for using Mercurial instead of Git (which was not as aggressible marketed in 2008 as now so there was a genuine choice to be made): (1) Mercurial emphasizes a nice semantic model of monotonic history and immutable changes (in coincidence with the Isabelle/ML approach and the then emerging PIDE document model). (2) Mercurial was positioned as a nice Python library/API, not a collection of shell scripts and C-programs. We even had a perspective to make Pyhton our main "lambda calculus approximation for system programming". Mira is fully on that line, although the "lambda calculus" of Python turned out as very approximative indeed. So both has shifted a bit over time. Influenced by the crowds behind Git, Mercurial has made non-monotonic operations more easily accessible than before, say via some "rebase" option to formerly pure hg commands. Thus it is no longer obvious which operations are pure and which are impure. (The emerging DVCS GUI front-ends help out a bit here.) 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 http://hg4j.com/ are not very far yet. Also interesting is http://mercurial.selenic.com/wiki/CommandServer which is a third way to the API vs. external executable problem: some hg process is started once and used with a certain protocol over the pipe. I would like to see a Scala wrapper for that ... Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Reasons mira crashes
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 unreliable. I've been thinking of this occasionally, but it does not work either, because the "gateway" systems that are reachable for ssh from outside are fluctuating a lot. It used to be just atbroy100 as canonical example some years ago, then one had to shuffle macbroy20..29 to get some machine that happens to be available, now one occasioanlly needs to take the lxlabbroy into account. I edit my .hg/hgrc a lot these days. 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 =) So if there is an easy solution to more robust access of some file system served at TUM, I am for it. Anything beyond that should be a move away from home-made servers to some professional hosting platform like Bitbucket (not Sourceforge, not Google code). Note that we have already several home-made services running that are only half-maintained, and we cannot afford this for the main collection point of Isabelle changesets. I will ask the MTAs about that. Since some time they also provide hosting of mercurial repositories. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Reasons mira crashes
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 "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 unreliable. I've been thinking of this occasionally, but it does not work either, because the "gateway" systems that are reachable for ssh from outside are fluctuating a lot. It used to be just atbroy100 as canonical example some years ago, then one had to shuffle macbroy20..29 to get some machine that happens to be available, now one occasioanlly needs to take the lxlabbroy into account. I edit my .hg/hgrc a lot these days. On Wed, 28 Nov 2012, Makarius wrote: On Wed, 28 Nov 2012, Gerwin Klein wrote: This may be entirely unrelated, but I've just had to re-clone the afp hg repository in my home directory at TUM because it made mercurial crash on pull, and failed integrity checking. The only other time I've ever had to do that in the past few years of using mercurial was because of file corruption due to a broken hard disk (two cases). If this happens frequently to us, something may be very wrong with storage on the macbroy/lxbroy machines. The reliability of NFS at TUM has indeed degraded a bit, maybe already more than 5 years ago, but it is hard to pin down. I now remember the difference from distant past. Until approx. 5-6 years ago, the NFS server (first sunbroy60, then sunbroy1, then sunbroy2) was accessible by ssh. Thus everybody was using that for his ssh login in the cvs configuration, because it made things much faster with the local harddisk access on the remote host. So neither the NFS problem nor the client program confusion did exist. Then the NFS server was made more "secure", so users could no longer login. I also remember now that it was the point where cvs became unbearably slow, and thus accelerated our move to state-of-the-art version control, where central transactions only happen occasionally (pull, push) and not for every single commit (which is hard to imagine now). So if there is an easy solution to more robust access of some file system served at TUM, I am for it. Anything beyond that should be a move away from home-made servers to some professional hosting platform like Bitbucket (not Sourceforge, not Google code). Note that we have already several home-made services running that are only half-maintained, and we cannot afford this for the main collection point of Isabelle changesets. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
