Re: [isabelle-dev] Use HTTPS for components

I agree, we should do that. Ideally, we should actually sign those components. The downloading/receiving/checking side is not too hard to automate, but it would require entering the private key keyphrase when you are signing (providing) a new component. Cheers, Gerwin > On 13 Jul 2016, at

Re: [isabelle-dev] Build NEWS

On 11 Jul 2016, at 16:03, Johannes Hölzl wrote: > > Am Sonntag, den 10.07.2016, 22:37 +0200 schrieb Lars Hupel: >> Dear AFP developers, >> >> some of you may have noticed that the "AFP devel" pages have not been >> updated since April. This is partly my fault because I migrated

Re: [isabelle-dev] An experience report on the testboard

> On 5 Jul 2016, at 16:15, Lars Hupel wrote: > >> Another way of getting simultaneous tests would be to use subrepos. I.e. >> >> test-repo/ >> isabelle/ (subrepo) >> afp/ (subrepo) >> >> The trigger would then be the push to test-repo, not to any of the subrepos, >> and

Re: [isabelle-dev] An experience report on the testboard

Another way of getting simultaneous tests would be to use subrepos. I.e. test-repo/ isabelle/ (subrepo) afp/ (subrepo) The trigger would then be the push to test-repo, not to any of the subrepos, and you would get a predictable combination as well. Cheers, Gerwin > On 5 Jul 2016,

Re: [isabelle-dev] AFP config files?

This specific entry currently exists only in devel. Release is clean. Cheers, Gerwin > On 23.06.2016, at 17:54, Lars Hupel wrote: > >> This is my entry. I submitted it a few days ago, and I included the >> config file in my submission. I was not aware that those don't exist

Re: [isabelle-dev] Discovering named_theorems

> changeset: 63080:8326aa594273 > tag: tip > user:wenzelm > date:Tue May 10 22:25:06 2016 +0200 > files: src/Pure/Isar/proof_context.ML > src/Pure/Tools/find_theorems.ML src/Pure/facts.ML > description: > find dynamic facts as well, but static ones are preferred; >

Re: [isabelle-dev] Odd branches on AFP

Thanks for closing that branch again. As Salomon explained it was accidental, but just in case there was unclarity about it for others: the afp development model is to not use mercurial internal branches, but forks and repository merges instead. Perfectly fine to use branches in your own copy

Re: [isabelle-dev] Additional lemma for Bool_List_Representation

I’ll transform the proof slightly and add it. Names are hard ;-) I’d call it just bl_to_bin_lt2p_drop. Cheers, Gerwin > On 23.03.2016, at 02:48, C. Diekmann wrote: > > Hi, > > in HOL/Word/Bool_List_Representation.thy, there is the lemma bl_to_bin_lt2p: > "bl_to_bin bs <

Re: [isabelle-dev] Jenkins maintenance window

How about pushing feature branches instead? Cheers, Gerwin > On 16 Feb 2016, at 09:25, Lars Hupel wrote: > >> tonight between 20:00 UTC and 22:00 UTC there will be a maintenance >> window for the Jenkins instance. > > Maintenance period is over now. All builds are running

Re: [isabelle-dev] Status of afp-devel wrt. release?

The official status is: afp-2016 is now forked and preparing for release. Any new changes to afp-devel will stay on afp-devel by default and it is fine to move on with isabelle-dev. Everything I’m aware of on afp-2016 is concluded, but if anyone still has change sets that really need to move

Re: [isabelle-dev] Multicore timings

Nice! I distinctly remember the times when MicroJava was a very long session ;-) Cheers, Gerwin > On 15 Jan 2016, at 11:16 AM, Makarius wrote: > > Just for the record here are some timings on dual Xeon E5-2620v3 2.40GHz with > 12 threads: > > Isabelle/9ca00b65d36c +

Re: [isabelle-dev] find_theorems and type class axioms

I agree, we should do something about it. All relevant people on our side currently are pretty busy with a project deliverable for 1st Dec, but we should be able to give find_theorems some of the TLC it deserves after that. This may not be easy to solve - it probably is just how

Re: [isabelle-dev] NEWS: State panel

> On 9 Nov 2015, at 9:41 pm, Makarius wrote: > > * The State panel manages explicit proof state output, with jEdit action > "isabelle.update-state" (shortcut S+ENTER) to trigger update according > to cursor position. > > * The Output panel no longer shows proof state output

Re: [isabelle-dev] isatest/afptest logs

Under the account isatest in ~/afp/log and ~/log. Cheers, Gerwin > On 20.10.2015, at 19:09, Lars Hupel wrote: > > Dear developers, > > does anyone know where the isatest and afptest logs are stored? I'd like > to do some performance analysis over the last, say, one month. (If

Re: [isabelle-dev] AFP/Lifting_Definition_Option

see now that even this didn't happen: I guess I assumed that René would > do it and he assumed that I would do it. This is my fault. I should have made > this assumption clearer. > > Bests, > Ondrej > > On 10/05/2015 11:33 PM, Gerwin Klein wrote: >> The first step

Re: [isabelle-dev] AFP/Lifting_Definition_Option

The first step would be to contact the authors of the entry. If they agree that it is superseded by something else, the entry can be made empty, with an explanation/referral to whatever replaced it. Cheers, Gerwin > On 06.10.2015, at 03:15, Makarius wrote: > > What is the

Re: [isabelle-dev] status (AFP)

I think you might have accidentally pushed to afp-2015 instead of afp-devel. This is on afp-2015: changeset: 5536:b0b40e683dbc user:paulson l...@cam.ac.uk date:Thu Aug 20 17:31:45 2015 +0100 summary: fixed problems mostly connected with changes to tendsto_zero_powrI I’ll

Re: [isabelle-dev] Remaining uses of defer_recdef?

papers. Short summary, NICTA doesn't have any stakes in recdef. Cheers, Thomas. On 08/06/15 06:13, Makarius wrote: On Sat, 6 Jun 2015, Gerwin Klein wrote: On 06.06.2015, at 21:23, Makarius makar...@sketis.net wrote: (2) 'defer_recdef' which is unused in the directly visible Isabelle

Re: [isabelle-dev] Status of afp-2015

You’re right, it is currently not tested automatically. I was going to set this up on the weekend, but didn’t manage to. As far as I’m aware, there weren’t any commits to afp-2015 after the fork apart from one update that was a leaf node that I checked manually. Isabelle-RC has moved, though.

Re: [isabelle-dev] Status of afp-2015

. I don’t expect that things will break much, though. Cheers, Gerwin On 28 Apr 2015, at 7:26 pm, Makarius makar...@sketis.net wrote: On Tue, 28 Apr 2015, Gerwin Klein wrote: You’re right, it is currently not tested automatically. I was going to set this up on the weekend, but didn’t manage

Re: [isabelle-dev] docs for new datatype package

On 21 Apr 2015, at 6:07 pm, Jasmin Blanchette jasmin.blanche...@inria.fr wrote: (Independent of all this, it would be nice if the primrec package did that declaration now automatically in any case) Again, I believe it does: primrec (nonexhaustive) f and fs and g and gs where f

Re: [isabelle-dev] docs for new datatype package

On 21 Apr 2015, at 6:07 pm, Jasmin Blanchette jasmin.blanche...@inria.fr wrote: But when it comes to “size”, I’m sorry I didn’t make it more compatible with the old one. Thankfully, there’s an easy (if tedious) workaround. Just found out that datatype_compat does declare the old size

Re: [isabelle-dev] docs for new datatype package

On 21 Apr 2015, at 9:19 pm, Jasmin Blanchette jasmin.blanche...@inria.fr wrote: The swapping is consistent in the sense that the order in the rule itself doesn’t really change, but the order in which the rule expects the properties in the goal is what leads to the swapping. The induction

Re: [isabelle-dev] docs for new datatype package

Maybe datatype_compat is the one I should go with for now. Need to check if that has an influence on the induction order. “datatype_compat” should give exactly the same induction principle as before, modulo naming of its schematic variables, even in the presence of 4-way nesting. After

Re: [isabelle-dev] docs for new datatype package

, On 19.04.2015, at 16:45, Gerwin Klein gerwin.kl...@nicta.com.au wrote: The datatype manual says in e8472fc02fe5: The datatype_compat command is needed to register new-style datatypes for use with fun and function (Section 2.2.2) Is this still correct? Indeed, this is a couple of versions behind

[isabelle-dev] docs for new datatype package

The datatype manual says in e8472fc02fe5: The datatype_compat command is needed to register new-style datatypes for use with fun and function (Section 2.2.2) Is this still correct? Cheers, Gerwin The information in this e-mail may be confidential and subject

Re: [isabelle-dev] NEWS: Z3 open source

Despite such routine improvements, many users will probably just stick to old habits from the TTY age, and put the sledgehammer command into the text. (Are there remaining uses of this ancient form? Or are there still pending problems with the current Sledgehammer panel?) I don’t think

Re: [isabelle-dev] AODV

On Wed, 10 Dec 2014, Tobias Nipkow wrote: On 09/12/2014 21:50, Makarius wrote: On Wed, 10 Dec 2014, Gerwin Klein wrote: “build -a” is still going to miss document preparation errors in the AFP, though, so it’s still not really the right command to run for testing it. We've

Re: [isabelle-dev] AODV

Back to afp_build: I merely made that in 2012 as an example how to map the old shell scripts to the new Isabelle build setup. I never use afp_build myself, but just plain isabelle build. One day I also hope to be able to load all of AFP into a single PIDE session, to edit it without

Re: [isabelle-dev] AODV

Only the “everything” session should ever be run in a normal test, the other sessions are for convenience while developing only. This is why AODV is in group “AFP” and the others are not. There are other entries that have similar setup, i.e. “build -a” will usually do too much. The best way to

Re: [isabelle-dev] Abbreviations and find_theorems

Hi Florian, I'm not worried about the eta conversion and am happy with your solution on that one. The abstraction expansion worried me more, but since I seem to be the only one who makes use of crazy patterns that would benefit from it not being there, let's go with your solution there as

Re: [isabelle-dev] Duraraion of AFP session AODV

Not sure about lxbroy10, but AODV is now the longest session. It takes about 1:40h on my machine (needs less memory than JinjaThreads, though). Cheers, Gerwin On 27.11.2014, at 05:10, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: How long is session AODV expected to

Re: [isabelle-dev] Abbreviations and find_theorems

I agree that it would be nice to support that, esp since find_theorems is supposed to help beginners find things. Applying underscores will have unwanted side effects for other terms, esp constants, though, so one would have to be careful to apply this to abbreviations only. AFAIR this is the

Re: [isabelle-dev] porting code to isabelle2014 and getting unfinished linear change errors

It’s entirely possible that the tests for Simpl in the AFP need improvement - the current VCG examples may not be using the full range of commands it provides. Greetings from Kununurra somewhere in WA, Gerwin On 26 Aug 2014, at 1:51 pm, Michael Norrish michael.norr...@nicta.com.au wrote:

Re: [isabelle-dev] Towards the Isabelle2014 release

On 10.08.2014, at 11:13 pm, Makarius makar...@sketis.net wrote: Note that isatest and AFP are still hooked on Isabelle2014-RC, until Gerwin points out the schedule for the correlated AFP release fork. We’ll do the inverse of the usual process: we’ll fork afp very soon. Since the

Re: [isabelle-dev] Fwd: [isabelle] seL4 open source

environment or something similar, this seems to be a nice candidate for inclusion. Florian Forwarded Message Subject: [isabelle] seL4 open source Date: Tue, 29 Jul 2014 10:55:45 + From: Gerwin Klein gerwin.kl...@nicta.com.au To: USR Isabelle Mailinglist isabelle-us

Re: [isabelle-dev] Remaining uses of Proof General?

On 25 Jul 2014, at 10:23 am, Makarius makar...@sketis.net wrote: Oddly, people are still seen using 'find_theorems' etc. inlined into the source text. That was an intermediate approach from several years ago. If it is still used today, what are the remaining resons for it? Not having to

Re: [isabelle-dev] Remaining uses of Proof General?

On 25 Jul 2014, at 11:20 am, Makarius makar...@sketis.net wrote: On Fri, 25 Jul 2014, Gerwin Klein wrote: On 25 Jul 2014, at 10:23 am, Makarius makar...@sketis.net wrote: Oddly, people are still seen using 'find_theorems' etc. inlined into the source text. That was an intermediate

Re: [isabelle-dev] ISABELLE_GHC/quickcheck

that are set up such that they are tested only if ISABELLE_GHC is set. Therefore, there cannot be an error message about quickcheck narrowing if ISABELLE_GHC is not set. Andreas On 19/07/14 21:30, Gerwin Klein wrote: Just had a very strange experience with ISABELLE_GHC. You will have

[isabelle-dev] ISABELLE_GHC/quickcheck

Just had a very strange experience with ISABELLE_GHC. You will have noticed that the AFP test failed the last few days with GHC compilation errors. The AFP test settings included the line ISABELLE_GHC=/opt/local/bin/ghc Apparently, this caused sessions like Native_Word to fail, even though

Re: [isabelle-dev] Towards the Isabelle2014 release

Good point. Tom, if you send me the text I will update the two files. Cheers, Gerwin On 3 Jul 2014, at 10:30 pm, Makarius makar...@sketis.net wrote: On Thu, 3 Jul 2014, Gerwin Klein wrote: Applied cleanly and is now pushed. On 3 Jul 2014, at 9:55 am, Thomas Sewell thomas.sew

Re: [isabelle-dev] Towards the Isabelle2014 release

. From: Makarius [makar...@sketis.net] Sent: Monday, June 30, 2014 9:56 PM To: Gerwin Klein; Thomas Sewell Cc: isabelle-dev@mailbroy.informatik.tu-muenchen.de Subject: Re: [isabelle-dev] Towards the Isabelle2014 release On Wed, 11 Jun 2014, Gerwin Klein wrote: On 11.06.2014

Re: [isabelle-dev] AFP: Failing entries

Thanks for that. It’s good to have them all back to green. Cheers, Gerwin On 30 Jun 2014, at 11:20 am, Peter Lammich lamm...@in.tum.de wrote: Finally, (after I have found out how to use afp_build) I could reproduce and fix the docuemnt preparation errors in the CAVA-entries, and now,

Re: [isabelle-dev] AFP: Failing entries

Hi Peter, thanks for the update. The last few days have seen isatest failures. The AFP test only runs when isatest is successful on polyml. The last failure that I saw (today) was on the smlnj platform only, so if nothing else goes wrong it should run through today. Cheers, Gerwin On

Re: [isabelle-dev] [isabelle] New AFP entry: Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions

Thanks for that. I’ve just merged it and since you have a patch already not attempted to repair. Cheers, Gerwin On 13.06.2014, at 6:27 pm, Dmitriy Traytel tray...@in.tum.demailto:tray...@in.tum.de wrote: I'm following the suggestion of announcing who will fix a new AFP entry for the

Re: [isabelle-dev] AFP failures near 7f7ca3a43026

On 12.06.2014, at 6:11 pm, Jasmin Christian Blanchette jasmin.blanche...@gmail.com wrote: Am 12.06.2014 um 00:58 schrieb Gerwin Klein gerwin.kl...@nicta.com.au: In the first instance, it is the authors/maintainers of the entry that we will ask for help. In this case, Peter has promised

Re: [isabelle-dev] AFP failures near 7f7ca3a43026

On 12.06.2014, at 7:52 pm, Jasmin Christian Blanchette jasmin.blanche...@gmail.com wrote: Maybe the reporting should change to highlight new failures more prominently. Right. Or a has this entry ever worked or even a date indicating when the entry last succeeded. Ok, I'll have a look at

Re: [isabelle-dev] Towards the Isabelle2014 release

On 11.06.2014, at 2:56 pm, Thomas Sewell thomas.sew...@nicta.com.au wrote: Gerwin will push the isabelle hypsubst change to the testboard now (assuming he can remember how). He could and did. Cheers, Gerwin The information in this e-mail may be

Re: [isabelle-dev] neg_numeral fallout

Looks ok, but what about all the other operators? (shift, rotate, etc) Cheers, Gerwin On 16 May 2014, at 8:25 pm, Lars Noschinski nosch...@in.tum.de wrote: (moving this to the -dev list): On 15.05.2014 18:59, Florian Haftmann wrote: Hi Lars, when you abolished neg_numeral, the lemmas in

Re: [isabelle-dev] status (AFP)

The problem seems to be HyperCTL. From the log: Run out of store - interrupting threads Failed to recover - exiting /tmp/isabelle-isatest/isabelle_script3270098471353362986: line 8: /mnt/nfsbroy/home/isatest/afp/isadist/Isabelle_04-May-2014/lib/scripts/timestop.bash: No such file or directory

Re: [isabelle-dev] HOL-Decision_Procs FAILED

On 18 Mar 2014, at 10:23 pm, Makarius makar...@sketis.net wrote: Maybe I should try to improve the implicit rule method to reveal the rule that was applied --- via a form of semantic completion. It is a bit more difficult than the other completions so far, because there is also the lazy

Re: [isabelle-dev] smt2

On 15.03.2014, at 2:39 am, Makarius makar...@sketis.net wrote: On Fri, 14 Mar 2014, Andreas Lochbihler wrote: IIRC, the AFP policy is (was?) that all entries that import at least one theory from HOL-Library are based on HOL-Library. I can't speak for the AFP editors, but that might be

Re: [isabelle-dev] Hg sourcetree

I have it installed and it's nice for browsing through history, but for normal daily operation I still find myself using primarily the command line, mostly because it's quick and I'm used to it. Cheers, Gerwin On 19 Dec 2013, at 6:26, Makarius makar...@sketis.net wrote: Since I am

Re: [isabelle-dev] Broken / dead theories in AFP

Thanks for spotting that, I will have a look at these. Cheers, Gerwin On 12 Dec 2013, at 11:36 pm, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: hg id 3b70f59667aa Launchbury/Down.thy Launchbury/LaunchburyUnBH.thy -- PGP available:

Re: [isabelle-dev] Isabelle2013-2 release

On 21.11.2013, at 10:56 pm, Makarius makar...@sketis.net wrote: Did anybody test WWW_Find? Have just confirmed that WWW_Find works fine with Isabelle2013-2-RC2 Cheers, Gerwin The information in this e-mail may be confidential and subject to legal

Re: [isabelle-dev] AFP failures

On 26 Nov 2013, at 11:44 pm, Makarius makar...@sketis.net wrote: This means, by rearranging certain library sessions, AFP documents suddenly include theories into the document that are not meant to be there. We don't have a systematic check for this, so AFP documents are generally

Re: [isabelle-dev] Isabelle2013-2 release

Sorry, missed all this, because I was away (and the rest of NICTA had a quite busy week). On 21.11.2013, at 10:56 pm, Makarius makar...@sketis.net wrote: On Wed, 20 Nov 2013, Makarius wrote: Did anybody test WWW_Find? WWW_Find is a NICTA-only tool. Did any of the NICTA guys test it in

Re: [isabelle-dev] Ordinary_Differential_Equations FAILED

Yes, you can commit freely to AFP-devel. Cheers, Gerwin On 31 Oct 2013, at 9:33 pm, Fabian Immler imm...@in.tum.de wrote: Hi, complete_univ has been renamed to complete_UNIV in Isabelle 1a13325269c2 (after the fork for the release). I therefore assume that I can commit the relevant

[isabelle-dev] AFP 2013-1 release branch

Following the Isabelle release candidates, the AFP now also has a separate release branch for 2013-1. Commits to devel will go into the normal development version and not show up in this release branch. Basically, business can continue as usual for Isabelle developers. mira is testing

Re: [isabelle-dev] jdk-7u40

On 14/09/2013, at 6:50 AM, Makarius makar...@sketis.net wrote: For example, they say that Apple Retina displays are now fully supported. Can people who are so lucky to have one test that, and say if it works, or if it requires further Java properties? The isabelle jedit tool allows to pass

Re: [isabelle-dev] Isabelle_10-Sep-2013

On 12/09/2013, at 3:02 AM, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: I just downloaded the compiled binary for Linux and wanted to share my experience. It seems there are some issues with braces. My thy files work fine with the release, however, in the AFP

Re: [isabelle-dev] HOL iff notation

On 03/09/2013, at 12:24 AM, Makarius makar...@sketis.net wrote: Are there clubs of iff vs. non-iff? If almost everybody is a member of the iff club we could just remove that print mode. (We don't have to consider that for the coming release, to avoid any real-time pressure on this

Re: [isabelle-dev] NEWS: Dockable window Find

On 09/08/2013, at 9:17 PM, Makarius makar...@sketis.net wrote: On Fri, 9 Aug 2013, Gerwin Klein wrote: Is this special Duplicates treatment still relevant? Yes, it's still relevant. One of the uses of the command where duplicates are reported is to see how often the same theorem is proved

Re: [isabelle-dev] NEWS: Dockable window Find

On 10/08/2013, at 9:09 AM, Gerwin Klein gerwin.kl...@nicta.com.au wrote: I like the interface, it's very responsive. There is a remnant from PG times: the best match is currently the last entry in the list, which means in jEdit that you need to scroll to see it. Should we automatically

Re: [isabelle-dev] NEWS: Dockable window Find

, Gerwin On 10/08/2013, at 11:19 AM, Gerwin Klein gerwin.kl...@nicta.com.au wrote: On 10/08/2013, at 9:09 AM, Gerwin Klein gerwin.kl...@nicta.com.au wrote: I like the interface, it's very responsive. There is a remnant from PG times: the best match is currently the last entry in the list

Re: [isabelle-dev] Subscripts within identifiers

On 08/08/2013, at 9:18 PM, Makarius makar...@sketis.net wrote: Together with our \^sub\omega this reconfirms my initial impression that it is better to have the asymmetry of \^sub for identifiers vs. \^sup for notation. As a consequence, \twosuperior also becomes obsolete; \onesuperior

Re: [isabelle-dev] NEWS: Dockable window Find

On 09/08/2013, at 9:05 PM, Makarius makar...@sketis.net wrote: *** Prover IDE -- Isabelle/Scala/jEdit *** * Dockable window Find provides query operations for formal entities (GUI front-end to 'find_theorems' command). This sounds cool, will try it out soon. Anyway, what is the purpose

Re: [isabelle-dev] Sum_of_Squares_Remote failure

Tobias and I just tried from a laptop on version 41ebc19276ea, which seems to work fine. Has somebody fixed it in the meantime? Gerwin On 07/08/2013, at 3:21 PM, Makarius makar...@sketis.net wrote: The remote Sum_of_Squares tests keeps failing (for about one week already, today we are at

Re: [isabelle-dev] Proposing extensions to the Isabelle library?

The AFP web view doesn't seem to be down from here. The change set is this one, I think: http://sourceforge.net/p/afp/code/ci/b1e24b9aaa77a61c7b199cdb6f21aaef3492c0c1/ Cheers, Gerwin On 25/07/2013, at 9:10, Florian Haftmann

Re: [isabelle-dev] Proper AFP history on the web

On 12.07.2013, at 9:09 PM, Makarius makar...@sketis.net wrote: On Wed, 10 Jul 2013, Gerwin Klein wrote: The official URL for browsing is http://sourceforge.net/p/afp/code/ci/default/tree/ as advertised on http://afp.sourceforge.net/download.shtml. That tree view is what I meant as old

Re: [isabelle-dev] Proper AFP history on the web

I don't think that's a good idea. The official URL for browsing is http://sourceforge.net/p/afp/code/ci/default/tree/ as advertised on http://afp.sourceforge.net/download.shtml. The official URL for cloning is http://hg.code.sf.net/p/afp/code as advertised on that page (with ssh and SF login

Re: [isabelle-dev] Formatting AFP Devel-Entries

On 18/06/2013, at 9:15 PM, Christian Sternagel c.sterna...@gmail.com wrote: On 06/18/2013 02:23 PM, Gerwin Klein wrote: On 17/06/2013, at 12:45 PM, Lars Noschinski nosch...@in.tum.de wrote: A more severe problem is that the URLs in the BibTeX data are wrong (both for devel and release

Re: [isabelle-dev] Formatting AFP Devel-Entries

Hi Lars, thanks for spotting that. I know what's going wrong (I'm parsing isabelle build output wrong), and I have a more fundamental fix for it almost ready to go, but it's on my computer at home which I can't access while travelling. I'll be back end of June and will push it then. Cheers,

Re: [isabelle-dev] Formatting AFP Devel-Entries

On 17/06/2013, at 12:45 PM, Lars Noschinski nosch...@in.tum.de wrote: A more severe problem is that the URLs in the BibTeX data are wrong (both for devel and release), they are missing the .shtml suffix. Thanks. How embarrassing. These are fixed now in the release version and should pop up

Re: [isabelle-dev] AFP sitegen

On 06.06.2013, at 1:52 PM, Gerwin Klein gerwin.kl...@nicta.com.au wrote: I'll have a look at it. The links shouldn't be dropped, something is going wrong there. Cheers, Gerwin On 06/06/2013, at 1:48 PM, Christian Sternagel c.sterna...@gmail.com wrote: Btw: the links do not seem to work

Re: [isabelle-dev] AFP sitegen

I'll have a look at it. The links shouldn't be dropped, something is going wrong there. Cheers, Gerwin On 06/06/2013, at 1:48 PM, Christian Sternagel c.sterna...@gmail.com wrote: Btw: the links do not seem to work anyway. But why not replace them with working links instead of just dropping

Re: [isabelle-dev] I don't understand isatest AFP report

On 15.05.2013, at 8:01 PM, Ondřej Kunčar kun...@in.tum.de wrote: Hi! This is the last report about AFP from isatest: The status of the following AFP entries changed or remains FAIL: [Containers] was removed. Last status was ok. [Launchbury] is new. Status is ok. Full entry status at

Re: [isabelle-dev] Global build failures of the AFP in the testboard

On 16.05.2013, at 1:25 AM, Lars Noschinski nosch...@in.tum.de wrote: @Alex, Gerwin: Is there any reason remaining why the AFP should not use the default PolyML version? I remember Alex and I dropped a similar override from the Isabelle tests. Not that I am aware of. The main reason there

Re: [isabelle-dev] I don't understand isatest AFP report

On 15.05.2013, at 11:33 PM, Makarius makar...@sketis.net wrote: On Wed, 15 May 2013, Gerwin Klein wrote: What's going on is that the somewhat primitive AFP test doesn't understand the output of isabelle build correctly. It's currently getting its list of sessions by scanning through

Re: [isabelle-dev] [PATCH 0 of 1] Fix top-level printing of exception messages containing forced-line breaks

On 04/04/2013, at 12:42 PM, Makarius makar...@sketis.net wrote: On Thu, 4 Apr 2013, Thomas Sewell wrote: David's investigation explains a problem we had a few years ago where some custom tactics of mine were killing my colleagues' ProofGeneral sessions when they encountered errors. The

Re: [isabelle-dev] AFP access confusion

On 23/03/2013, at 2:05 PM, René Thiemann rene.thiem...@uibk.ac.at wrote: I recently got some message from sourceforge, that they changed their directory structure. So I have no problems accessing the afp at ssh://login@hg.code.sf.net/p/afp/code Everybody with access to the AFP repository at

Re: [isabelle-dev] Feature suggestion: apply (meth[1!])

On 11/03/2013, at 11:42 AM, Makarius makar...@sketis.net wrote: On Mon, 11 Mar 2013, David Greenaway wrote: As a data point, inside the seL4 proof, a largish application of Isabelle, such a solve-or-fail mechanism would have been very helpful. So can you show the sources for that, to give

Re: [isabelle-dev] Post-release mode

On 13.02.2013, at 11:33 PM, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: Isabelle/0a55ac5bdd92 is the merge point for the release branch from https://bitbucket.org/isabelle_project/isabelle-release Now the main Isabelle repository is again the main focus for working

Re: [isabelle-dev] Post-release mode

On 14.02.2013, at 7:08 PM, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: what exactly is afp-devel? I am unable to map this to the repositories I am aware of (http://afp.hg.sourceforge.net/hgweb/afp/afp/shortlog, http://isabelle.in.tum.de/repos/AFP/) Sorry, that could

Re: [isabelle-dev] Fork of Isabelle2013 release repository TODAY

to the release branch around the deadline of the camera ready version (in case of acceptance *fingers crossed*) would also be nice (in case, reviews triggered changes in a formalization). Anyone else? On 01/22/2013 06:33 AM, Gerwin Klein wrote: On 21.01.2013, at 2:08 AM, Makarius makar

Re: [isabelle-dev] Fork of Isabelle2013 release repository TODAY

On 21.01.2013, at 2:08 AM, Makarius makar...@sketis.net wrote: * AFP needs to be understood wrt. isabelle-release. Gerwin will explain his organization of the AFP release for Isabelle2013, based on the afp-devel repository. I'll attempt to make the AFP release semi-simultaneous with

[isabelle-dev] Fwd: status (AFP)

The afp test is now back to normal operation and the devel website update is working again as well. The two below are real failures, possibly have been there for a while masked by the problems the test had. Cheers, Gerwin Begin forwarded message: From:

Re: [isabelle-dev] Must the AFP be used as a component? (was: Reasons mira crashes)

On 14/12/2012, at 6:55 PM, Lars Noschinski nosch...@in.tum.de wrote: The reason is that Open_Induction/ROOT (and also Open_Induction/Open_Induction.thy) relies on $AFP being set, which is only the case if AFP is registered as a component (which is not the case for Mira). @Gerwin: Since you

Re: [isabelle-dev] isatest silence

On 15/12/2012, at 12:54 AM, Makarius makar...@sketis.net wrote: The unusual isatest silence from today means that all tests finished successfully! No news are good news :-) http://isabelle.in.tum.de/devel/ shows some development snapshot Isabelle_14-Dec-2012.tar.gz together with the

Re: [isabelle-dev] AFP devel broken

On 29/11/2012, at 11:47 PM, Christian Sternagel c-ste...@jaist.ac.jp 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

Re: [isabelle-dev] Reasons mira crashes

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

Re: [isabelle-dev] isatest ssh

On 27/11/2012, at 12:55 AM, Makarius makar...@sketis.net wrote: On Mon, 26 Nov 2012, Gerwin Klein wrote: The reasoning (or rather hope) behind the above was that for doing real non-sense you would have to be on the local network at TUM. So it is basically a switch back towards the old

Re: [isabelle-dev] isatest ssh

On 20/11/2012, at 11:23 PM, Makarius makar...@sketis.net wrote: There is this recurrent game to have the isatest user do many manual ssh logins to update known_hosts. Getting tired of it, I just did some reading of man ssh_config and some googling. This resulted the following

Re: [isabelle-dev] AFP: Session AVL-Trees broken

If I run sessions manually, they work fine, but they fail in the cron job with timeout (even small ones like Separation_Algebra). This has been going on for a while. Does anyone have an idea what's going on? Is there something else running on macbroy2 at the same time that takes a lot of

Re: [isabelle-dev] AFP: Session AVL-Trees broken

On 08/11/2012, at 8:26 AM, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: Am 07.11.2012 22:22, schrieb Gerwin Klein: If I run sessions manually, they work fine, but they fail in the cron job with timeout (even small ones like Separation_Algebra). In the case of AVL

Re: [isabelle-dev] AFP: Session AVL-Trees broken

On 08/11/2012, at 8:50 AM, Lukas Bulwahn bulw...@in.tum.de wrote: On 11/07/2012 10:41 PM, Gerwin Klein wrote: I can see no reason why any of these would have to time out, and they don't on other machines (I've only tried some, though, not all). Could it be an artefact of time measurement

Re: [isabelle-dev] isabelle build for generating TeX Snippets

The approach in LaTeX Sugar is very similar, but I don't remember if we describe there how to avoid generating the superfluous pdf. You can basically use a script document/build that takes over control of which commands are run to build the document. That command could for instance just be

[isabelle-dev] isatest ~/.ssh/known_hosts

In an attempt to get rid of spurious Host key verification failed messages, I've cleaned out the old ~/.ssh/known_hosts file of isatest and manually re-added all hosts mentioned in Admin/isatest. If there are other things running under this account (mira?) that may break when ssh asks for host

Re: [isabelle-dev] status (AFP)

On 21/09/2012, at 9:31 PM, Makarius makar...@sketis.net wrote: On Fri, 21 Sep 2012, Tobias Nipkow wrote: This is just another reminder that people should watch the AFP when they check in changes, and fix them. The testboard runs most of the AFP. Once the testboard recovers, one could

Re: [isabelle-dev] usedir -P P http://isabelle.in.tum.de/library/

On 03/09/2012, at 10:15 PM, Makarius makar...@sketis.net wrote: On Sat, 1 Sep 2012, Gerwin Klein wrote: How do I do the equivalent of isabelle usedir -P URL in the new build system? I'm trying to make sure that generated HTML for AFP entries doesn't contain dangling links of the form

  1   2   >