Re: [isabelle-dev] ADTs in Scala

2012-04-14 Thread Lars Hupel
object Graph { // public operations to create ADT instances } final class Graph[Key, A] private(rep: SortedMap[Key, (A, (SortedSet[Key], SortedSet[Key]))]) { // implementation with access to rep } The main thing is the private in this odd position, which is

Re: [isabelle-dev] ADTs in Scala

2012-04-14 Thread Lars Hupel
I've heard of this recent addition to the OO vocabulary to fix some early conceptual problems of the approach. That is object Graph part only. How would a Java person solve the private constructor problem? Could you explain a bit more? -- Java has private constructors. The source file

Re: [isabelle-dev] Broken component: jdk7u40

2013-09-17 Thread Lars Hupel
We've had such incidents before with these huge jdk components. I had informed the local administrators about it, but they did not have any idea what could be wrong with the http server -- they made a reboot but it did not change substantially. If anyone wants to investigate further --

Re: [isabelle-dev] Broken component: jdk7u40

2013-09-30 Thread Lars Hupel
I also tried to download jdk7u40 today (twice), and ran into the very same problem. Maybe someone should check the configuration of the web server? I just mailed the local sysadmins about that issue. Since this seems to occur every now and then, we'll have to investigate that further. I'll

Re: [isabelle-dev] Isabelle2013-2 release

2013-11-21 Thread Lars Hupel
In an earlier message on this thread, you have posted a patch. However, I cannot apply this patch to the development repository, nor does the revision db3d3d99c69d, which your patch refers to, exist. I suppose db3d3d99c69d is the id of the patch itself, and it has already been applied on top

Re: [isabelle-dev] Isabelle2013-2 release

2013-11-25 Thread Lars Hupel
Another approach is to have the whole prover process running remotely, similar to the ancient rsh mode of Proof General 2.x that is forgotten now. Isabelle/Scala uses actors for internal communication, and this needs to be upgraded soon to one of the newer actor frameworks, such as Akka --

Re: [isabelle-dev] NEWS: interactive simplifier trace

2014-03-06 Thread Lars Hupel
Hi Chris, In the Simplifier Trace panel itself I did not find out how to get any output. Only after pressing the Show Trace button a new window opens that contains the output. yes, this is working as intended. The panel itself only shows interactive questions to the user, and by default,

Re: [isabelle-dev] Mira still alive?

2015-04-13 Thread Lars Hupel
This raises the questions whether somebody is still seriously relying on mira or whether it it time to admit that this approach has failed after some initial enthusiasm in 2010/2011. I would still appreciate a less ambitious continuous integration testing environment for Isabelle etc. using

[isabelle-dev] State of the builds

2015-07-13 Thread Lars Hupel
Dear list, I went ahead with my additions to FSets (see now Isabelle/3ba16d28449d), but not before pushing the change to the testboard. There, I noticed that the HOLCF and IOA (and depending sessions) fail. The report [0] just says timeout with no indication what actually the problem was. I

Re: [isabelle-dev] simps_of_case and function types

2015-08-25 Thread Lars Hupel
Does anyone rely on the more liberal form ... = P (case x of ...) accepted at the moment? Yes, I do. Sorry :-) Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de

[isabelle-dev] copy_bnf

2015-10-29 Thread Lars Hupel
Dear Dmitriy, I like the new "copy_bnf" command a lot, especially to allow records to be used in nested recursion. However, after a record definition, I have to invoke the command manually*. I would like to propose that "record" gains an option to call it directly. So, instead of writing:

Re: [isabelle-dev] copy_bnf

2015-10-29 Thread Lars Hupel
> I guess the general question is, whether it is fine to add the plugin > infrastructure for (most of the) existing commands (e.g., definition, > typedef, record, fun), thus enabling us writing tools that extend the > command’s functionality (be them enabled by default or not). I am

Re: [isabelle-dev] test failed (Archive of Formal Proofs)

2015-11-17 Thread Lars Hupel
Hello Peter, > The email claims that this build includes my patch. according to the log the AFP id is e6d87060e398, which doesn't include your patch (82552632a098). Or are you talking about another patch? Cheers Lars ___ isabelle-dev mailing list

[isabelle-dev] isatest/afptest logs

2015-10-20 Thread Lars Hupel
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 you have them in your mail inbox, you can also forward them to me.) Cheers Lars ___

[isabelle-dev] New testing infrastructure

2015-10-13 Thread Lars Hupel
Dear Isabelle developers, as promised last week, I've been working on a new testing infrastructure for Isabelle. Here's what works now: * There is a live Jenkins instance at [1]. It is publicly available and runs on a virtual machine provided by the department's

Re: [isabelle-dev] http://isabelle.in.tum.de/reports/Isabelle

2015-10-06 Thread Lars Hupel
> What is the situation with mira reports? The website shows a default > Mercurial view, without any test results. The situation is that Mira (including testboard) appears to be broken beyond repair. On Monday, I have taken over responsibility for our continuous integration builds and am already

[isabelle-dev] Future of isatest/afptest

2015-11-18 Thread Lars Hupel
(moving to isabelle-dev) > In the various different isatest configurations for main Isabelle (not > AFP) we do indeed test normal situations, like threads=4 or threads=8, > alongside with abnormal ones like threads=1 or skip_proofs=true. This is definitely something which I will replicate in the

Re: [isabelle-dev] ML equality types

2015-09-10 Thread Lars Hupel
I use those frequently as a curried version of 'op =', e.g. 'filter (equal "..." o fst) ...'. Lars Le 10 septembre 2015 12:31:14 GMT+02:00, Florian Haftmann a écrit : >In src/Pure/library.ML, the signature still contains the discouraged >and

Re: [isabelle-dev] Future of isatest/afptest

2015-12-29 Thread Lars Hupel
Status update: > 2) virtual machines provided by LRZ > > LRZ offers cloud hosting of virtual machines. We could get an > allowance of 32 cores, although one single machine can only have 8 at > most (e.g. we could run 4 virtual machines with 8 cores each). This > severely constrains how we can

Re: [isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves

2015-11-19 Thread Lars Hupel
Hi Florian, > What is the reason for this? No access to suitable computing machines? currently, the "new" testboard only performs "makeall" on the distribution. As I wrote in my mail from yesterday, I'm working on it. I expect to be able to make a recommendation on how to reinstate regular

Re: [isabelle-dev] popup in ce6320b9ef9b

2015-11-19 Thread Lars Hupel
> Here is a minimal example, but I am at loss to explain what is going on > here. The usual reason for a term being annotated twice is that it is (type) checked twice. Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de

Re: [isabelle-dev] Future of isatest/afptest

2015-11-19 Thread Lars Hupel
> Reckon you could make the status of the builds somehow public? Definitely! There are already two jobs public at our Jenkins server: As soon as I add more jobs, they (and their output) will appear there. Unfortunately the old scheme of sending mails to

Re: [isabelle-dev] HOL-Codegenerator_Test error

2016-01-11 Thread Lars Hupel
> Just a reminder of the normal routine: push to the Isabelle repository > always requires a full "isabelle build -a" -- there is no way around it. The testboard still executes "isabelle build -a". It's not yet building the AFP, though, but it's on my list. Cheers Lars

Re: [isabelle-dev] HOL-Codegenerator_Test error

2016-01-12 Thread Lars Hupel
(Take the following with a grain of salt, it is the result of a cursory investigation.) As far as I can tell the current problem is a variation of §7.1. Here's an excerpt from the error log: [error] /tmp/foo/foo.scala:5687: ambiguous implicit values: [error] both method semiring_char_0_nat in

Re: [isabelle-dev] Build NEWS

2016-06-13 Thread Lars Hupel
> Is there any consolidated documentation »How to test changesets > before contributing« or the like? I must confess that I don't even > know where to push changesets to, it is somewhere buried in my > mailbox. See my original mail: > * As pointed out by Larry, navigation on the Jenkins pages

Re: [isabelle-dev] Build NEWS

2016-06-13 Thread Lars Hupel
> * The URLs to push to are IMHO best presented using an hgrc excerpt, e.g. > >> [paths] >> testboard = ssh://h...@bitbucket.org/isa-afp/afp-testboard >> >> [alias] >> push_to_testboard = push -f testboard > > That way the risk for accidental pushes is greatly reduced Good idea. > * AFAIS,

Re: [isabelle-dev] problem with Nominal in the AFP

2016-05-31 Thread Lars Hupel
> Incompleteness FAILED This problem has already been addressed. Makarius changed some Isabelle signatures in Isabelle/4d04e14d7ab8, and adapted AFP in d46ea7497f. Unfortunately it's currently impossible to perform atomic changes to both repositories. Cheers Lars

Re: [isabelle-dev] problem with Nominal in the AFP

2016-05-31 Thread Lars Hupel
> Apart from that, there is also a custom to push AFP changes a bit later > than the ones on the Isabelle repository. Maybe Jenkins can take this > somehow into account and not start tests on AFP immediately. I've thought about this. The problem is that the notion of "a bit later" is ill-defined.

[isabelle-dev] Repaired Card_Equiv_Relations

2016-05-26 Thread Lars Hupel
Hi, for some reason, Lukas' entry Card_Equiv_Relations broke and remains broken. Since I wasn't sure anyone was taking care of it, I pushed 4d10819509 to afp-testboard to rectify the issue. I'm writing this to avoid duplicate work. Cheers Lars ___

Re: [isabelle-dev] Jenkins maintenance

2016-06-22 Thread Lars Hupel
> over the weekend, there will be a scheduled maintenance on the build > infrastructure. As announced earlier, jobs will be migrated to a new > machine, but also the Jenkins server itself will move. It took longer than anticipated, but on the plus side, I didn't have to cancel anything. Jenkins

[isabelle-dev] Jenkins maintenance

2016-06-17 Thread Lars Hupel
Dear Isabelle developers, over the weekend, there will be a scheduled maintenance on the build infrastructure. As announced earlier, jobs will be migrated to a new machine, but also the Jenkins server itself will move. That means that for some time, - jobs may be run on two different machines at

Re: [isabelle-dev] AFP config files?

2016-06-23 Thread Lars Hupel
> 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 > anymore. They have been superseded by the "notify" configuration in the "metadata" file. If one AFP maintainer could please delete

[isabelle-dev] New mailing list: isabelle-ci

2016-02-08 Thread Lars Hupel
Dear Isabelle users & developers, as per the discussion on [isabelle-dev]* we created a new mailing list: Starting soon, the Jenkins build will post build failures of Isabelle and AFP (but not testboard!) to that list.

Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?

2016-02-13 Thread Lars Hupel
> I have now done this in Isabelle/705d4c4003ea. > > It means that ISABELLE_FULL_TEST no longer occurs in the main Isabelle > repository. The extra slow sessions are in ~~/src/Benchmarks, and only > tested by special background jobs that take care of that. (Presently none!) Thanks. I will add a

Re: [isabelle-dev] Supported Poly/ML versions

2016-02-13 Thread Lars Hupel
> This question is relevant for the transition of isatest to Jenkins: many > isatest jobs are there to run old Poly/ML versions, and these CPU cycles > could be spared or put into better use. Interesting, I wasn't even aware of that. > * Old Poly/ML 5.3.0 is still needed in rare situations to

Re: [isabelle-dev] SML/NJ

2016-02-13 Thread Lars Hupel
> With such a painfully slow and incomplete SML/NJ test, it is time to ask > the canonical question: > > Are there remaining uses of SML/NJ, or can it be discontinued now? I have mixed feelings about this. On one hand, supporting multiple compiler platforms keeps us honest, i.e. to make sure

[isabelle-dev] Mail on build failures

2016-01-31 Thread Lars Hupel
Dear Isabelle and AFP developers, currently, isatest and afptest send build failure notifications to specific people specified in a global list (isatest) or per entry (afptest). How should this work in the future? For isatest, I don't think this global list makes much sense. Rather failures

Re: [isabelle-dev] Maintenance work on Jenkins VM

2016-01-31 Thread Lars Hupel
> * archival of the build logs As a temporary solution, I have now configured Jenkins to retain all build logs. I've found some pointers how to make Jenkins store them into some database, but will need to investigate further. > * installing compilers and setting the various >

Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?

2016-01-31 Thread Lars Hupel
> The "ISABELLE_FULL_TEST" variable and "slow" group are somehow adhoc > measures to get meaningful interactive tests, without wasting too much > time. It probably makes sense to imitate that for "testboard" setups. The idea is to distribute the build load over multiple machines, since that

Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?

2016-01-31 Thread Lars Hupel
> Building with SML/NJ configuration is trivial. It would be "just another > job" in Jenkins. I'd just need to know about what to build precisely. > Can you explain to me what the ML_SYSTEM_POLYML variable means? I was speaking too early. Here's what I get when trying to build Pure with SML/NJ:

Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?

2016-02-01 Thread Lars Hupel
> Clustering weak nodes always requires more administrative efforts than > just one or two fat nodes without special tricks. This is technically correct, but not to the extent you're implying. Managing one more node with the current setup is literally just another line in the Ansible

Re: [isabelle-dev] Maintenance work on Jenkins VM

2016-02-01 Thread Lars Hupel
> Native_Word should work again in 203deaf5208d (see also 61aeecc4093d), > both with GHC 7.8 and GHC 7.10. Build is still running, but looks like it's working again. I'm pushing another item on my todo list: Print the relevant system information (e.g. compiler versions) in the log. Cheers Lars

Re: [isabelle-dev] Maintenance work on Jenkins VM

2016-01-30 Thread Lars Hupel
Hi Dmitriy, > What about having an additional afp_testboard repository where one could also > push -f changes. I am particularly interested in “slow” sessions there. definitely possible, pending a Scala script which performs this:

Re: [isabelle-dev] Maintenance work on Jenkins VM

2016-01-30 Thread Lars Hupel
Update: > - running makeall and AFP (without "slow" sessions) on every push to > Isabelle > - running slow sessions nightly > - utilize 4 workers (8 cores, 64 GB each) from the LRZ > - running AFP (without "slow" sessions) on every push to AFP > - running everything on every push to testboard

Re: [isabelle-dev] Maintenance work on Jenkins VM

2016-01-30 Thread Lars Hupel
> Still missing in the setup: > * cross-platform/cross-parameter testing > * archival of the build logs > * time series I forgot: * installing compilers and setting the various ISABELLE_GHC/ISABELLE_OCAMLC etc. for Codegenerator_Test ___ isabelle-dev

[isabelle-dev] Maintenance work on Jenkins VM

2016-01-30 Thread Lars Hupel
Dear list, I'm currently performing maintenance work on the Jenkins VM. The following things are planned for today: - running makeall and AFP (without "slow" sessions) on every push to Isabelle - running slow sessions nightly - utilize 4 workers (8 cores, 64 GB each) from the LRZ I've already

[isabelle-dev] Grouping ISABELLE_FULL_TEST?

2016-01-31 Thread Lars Hupel
As of 527488dc8b90, there are five sessions which contain theories that are only processed under ISABELLE_FULL_TEST=true: HOL-ex Sudoku HOL-Datatype_Examples Brackin IsaFoR Misc_N2M HOL-Word-SMT_Examples SMT_Tests HOL-Quickcheck_Benchmark Find_Unused_Assms_Examples

Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?

2016-02-02 Thread Lars Hupel
> What remains are various benchmarks. We could move these sessions to > ~~/src/Benchmarks and omit that directory in ~~/ROOTS. Thus it can be > included on demand like this: > > isabelle build -d '~~/src/Benchmarks' -a > > or like this: > > isabelle build -D '~~/src/Benchmarks' > > This

[isabelle-dev] Disabled Jenkins mails

2016-02-28 Thread Lars Hupel
Dear list, I have temporarily disabled all mails from Jenkins. I hope to re-enable them soon with less useless traffic. Apologies for the spam. Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de

Re: [isabelle-dev] Build failed in Jenkins: afp-repo-checkin #80

2016-02-25 Thread Lars Hupel
> I am keen to see performance figures that are stored persistently in a > very simple format that can be understood without any special tools. I've designed the infrastructure with that in mind. In the current setting, Jenkins retains the full build log files indefinitely. > At the same time,

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failed in Jenkins: afp-repo-checkin #80

2016-02-25 Thread Lars Hupel
> Forgive me if I’m overlooking something obvious, but the attached > message about a failure in the AFP doesn’t seem to include any clue > as to which of the 200+ entries actually failed. I spent a little > time poking around https://ci.isabelle.systems/jenkins/ without > learning anything more.

[isabelle-dev] Jenkins maintenance window

2016-02-15 Thread Lars Hupel
Dear Isabelle developers, tonight between 20:00 UTC and 22:00 UTC there will be a maintenance window for the Jenkins instance. No new build will be scheduled after 14:00 UTC. This ensures that nothing is running during the window. You can still push to testboard, but nothing will happen. I

Re: [isabelle-dev] Jenkins maintenance window

2016-02-15 Thread Lars Hupel
> 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 again. Mails are not yet sent to the mailing list, neither is there a benchmark job. The reason follows. There was some weirdness wrt

Re: [isabelle-dev] Jenkins maintenance window

2016-02-16 Thread Lars Hupel
> Was it me? I think I saw a warning to that effect, but with "-f" > (which is necessary since we're creating new heads) it's too late > once the warning is shown. I can easily change the trusty old script > I use to push to testboard to make sure I do it from my Isabelle > repository. If it

Re: [isabelle-dev] Maintenance work on Jenkins VM

2016-02-16 Thread Lars Hupel
Hi Dmitriy, > What about having an additional afp_testboard repository where one > could also push -f changes. I am particularly interested in “slow” > sessions there. for now I've created a job which runs everything but the slow sessions (so not quite what you wanted). The repository is:

[isabelle-dev] Formula_Derivatives FAILED: Cannot allocate memory

2016-02-17 Thread Lars Hupel
Despite increasing the ML heap size with "-H 2000", the session "Formula_Derivatives" is failing. The build VMs have 32 GB of RAM, so that shouldn't be a problem. Here are the relevant environment variables: ML_PLATFORM="x86-linux"

Re: [isabelle-dev] Formula_Derivatives FAILED: Cannot allocate memory

2016-02-18 Thread Lars Hupel
> The obvious explanation is a failing proof which keeps using up more and more > memory. Wouldn't that be deterministic, then? It only fails spuriously. ___ isabelle-dev mailing list isabelle-...@in.tum.de

Re: [isabelle-dev] Formula_Derivatives FAILED: Cannot allocate memory

2016-02-18 Thread Lars Hupel
> yes, I also saw this on testboard and was confused. I'm at a loss, too. Maybe Makarius can give some hints on what the cause could possibly be. I could increase the heap space even more, but not sure if that is a good idea. Cheers Lars ___

Re: [isabelle-dev] Formula_Derivatives FAILED: Cannot allocate memory

2016-02-19 Thread Lars Hupel
> Try adding a --stackspace argument to reserve space for thread stacks > and anything else. e.g. > ML_OPTIONS="--stackspace 200M" > This option keeps this space back whenever Poly tries to grow the heap > to avoid the heap using all the available memory. You may need to > experiment a bit with

Re: [isabelle-dev] Formula_Derivatives FAILED: Cannot allocate memory

2016-02-19 Thread Lars Hupel
>> Try adding a --stackspace argument to reserve space for thread stacks >> and anything else. e.g. >> ML_OPTIONS="--stackspace 200M" >> This option keeps this space back whenever Poly tries to grow the heap >> to avoid the heap using all the available memory. You may need to >> experiment a bit

Re: [isabelle-dev] Formula_Derivatives FAILED: Cannot allocate memory

2016-02-22 Thread Lars Hupel
> That suggests that you're running the 32-bit version of Poly/ML in which > case the heap is limited to around 3-3.5G by the system and the problem > you're having is the total 4G memory limit. Switch to the 64-bit > version as a starting point. I was assuming that with 32G of memory you > were

Re: [isabelle-dev] Formula_Derivatives FAILED: Cannot allocate memory

2016-02-21 Thread Lars Hupel
> Another possibility is to set the maximum heap size with --maxheap e.g. > ML_OPTIONS="--maxheap 28G" > If the application needs it Poly/ML will try to grow the heap to avoid > doing a lot of garbage collection. That can result in it crowding out > other parts of the system that also need

[isabelle-dev] java.lang.ExceptionInInitializerError when starting Isabelle/jEdit

2016-04-11 Thread Lars Hupel
Dear Makarius, I wanted to try out some of the changes you made in the past week, but unfortunately, I'm getting exceptions upon starting Isabelle/jEdit. 12:33:24 [main] [error] Plugin: java.lang.ExceptionInInitializerError 12:33:24 [main] [error] Plugin: at

Re: [isabelle-dev] java.lang.ExceptionInInitializerError when starting Isabelle/jEdit

2016-04-12 Thread Lars Hupel
> In Isabelle/cfbb6a5b427c it is done again differently, and hopefully in > a more robust way. Thanks, that seems to have resolved the matter. Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de

Re: [isabelle-dev] Jenkins updates

2016-03-21 Thread Lars Hupel
Hi Dmitriy, > thanks for your work. Unfortunately, currently pushing to testboard/isabelle > does not seem to trigger new builds. Is this related to the job renamings? good catch. Apparently we ran into a bug which I didn't notice in the testing environment. I'm working on resolving it. Cheers

Re: [isabelle-dev] Jenkins updates

2016-03-21 Thread Lars Hupel
> good catch. Apparently we ran into a bug which I didn't notice in the > testing environment. I'm working on resolving it. Looks like I could resolve this by scheduling manual builds. Enjoy the blinking balls again :-) Cheers Lars ___ isabelle-dev

[isabelle-dev] Jenkins updates

2016-03-19 Thread Lars Hupel
Dear Isabelle developers, I've made another round of changes to the Jenkins setup today. * There is now a nightly "benchmark" job which runs everything in ~~/src/Benchmarks, as promised [0]. * Due to more spurious failures, I've switched over the build machines to use 64bit. Previous

[isabelle-dev] Failures in HOL-Codegenerator_Test

2016-04-04 Thread Lars Hupel
Dear Isabelle developers, I've been keeping an eye on our Jenkins tests and we're almost stable. That is, most build go through without problems or fail because there are broken proofs. However, there's still the occasional unexplained "total failure of existence". The latest instance: Running

Re: [isabelle-dev] Remaining uses of isatest/afptest

2016-04-26 Thread Lars Hupel
> In best Isabelle tradition, I'm asking the question: Are there any > remaining uses of isatest or afptest? I'll take this as a no. > If not, I will contact our system administrators and ask them to shut > down the old infrastructure (over the course of the next one or two > months).** First

Re: [isabelle-dev] Jenkins downtime

2016-05-23 Thread Lars Hupel
> I will send another update on Monday when the upgrades went through. The upgrades should be done now. In case you get any suspicious mails, please forward them to me. Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de

Re: [isabelle-dev] Isabelle repository broken

2016-05-24 Thread Lars Hupel
> https://ci.isabelle.systems/jenkins shows many dark clouds and > thunderbolts, but I have no clue where to look precisely. Jenkins is a complex piece of software (much more complex than Isabelle), so it is indeed hard to figure out where to click. The best way to stay on top of the current

[isabelle-dev] Nonterminating AFP build

2016-05-11 Thread Lars Hupel
Isabelle/8326aa594273 AFP/ffea2c11f257 We appear to have an issue with nonterminating builds. See here: . I had to manually kill the running poly process. I'm not quite sure which session causes it, but it's possibly

Re: [isabelle-dev] Build NEWS

2016-04-17 Thread Lars Hupel
> Maybe this can be simplified further. The "slow" group in the main > Isabelle repository is now rather pointless, even counterproductive. > HOL-Proofs and its subsessions has become relatively fast compared to > other bulky sessions. > > E.g. Isabelle/65f279853449 on 12 cores with 6 threads per

Re: [isabelle-dev] Build NEWS

2016-04-20 Thread Lars Hupel
> * I'm still working on getting the build to be more stable (i.e., get rid > of spurious failures). I've had a productive discussion with Gerwin how to > achieve that. Looks like this has been achieved. I haven't seen any spurious failures again. Also, build logs are now archived. If you pushed

[isabelle-dev] Remaining uses of isatest/afptest

2016-04-21 Thread Lars Hupel
Dear Isabelle developers, our Jenkins instance is about to replace the last piece of missing functionality from afptest: sending mails to maintainers. Yesterday, I switched on "artifacts", which means Jenkins now builds & archives "browser_info" and PDF output. This can be witnessed e.g. here:*

[isabelle-dev] Build NEWS

2016-04-16 Thread Lars Hupel
Dear list, I'd like to summarize the recent progress in the build infrastructure. * I'm still working on getting the build to be more stable (i.e., get rid of spurious failures). I've had a productive discussion with Gerwin how to achieve that. * Once that is done, the build mails will get

[isabelle-dev] Use HTTPS for components

2016-07-12 Thread Lars Hupel
Dear Isabelle developers, all of the critical Isabelle infrastructure (even website mirrors) is reachable via HTTPS. For Jenkins, it's not so important. For executable code, it is very important. Hence I would like to propose a simple change in the global "etc/settings":

Re: [isabelle-dev] Build statistics

2016-08-10 Thread Lars Hupel
> I did not know of this JSON API yet. In Isabelle/74604a9fc4c8 there are > Isabelle/Scala operations to access that information. (It is an > interesting experience to work with these untyped JSON things; reminds > me of LISP expressions.) Having HTTP APIs is one of the perks of running standard

Re: [isabelle-dev] Build NEWS

2016-07-17 Thread Lars Hupel
> Anyway, there's now a reboot of these pages available at: > > > > Note that this is a preview: The status is still [skipped] everywhere > and most download links don't work. This will be fixed some time this week. This is now done, see for example

Re: [isabelle-dev] \nexists

2016-07-19 Thread Lars Hupel
>> How can I extract this information from within Isabelle/Scala? How would >> this information be presented? > > It is emitted into the session log file. Build.parse_log may serve as an > example how to access it. Is there no structured way of accessing this information? At least it's Scala but

Re: [isabelle-dev] \nexists

2016-07-15 Thread Lars Hupel
> Latex tests add very little information for the extra time. It is > usually easy to figure out what needs to be done to make a broken > document work again. Moreover, the test often fails because of bad latex > installations, not because of bad documents. I disagree. 0% of LaTeX failures

Re: [isabelle-dev] \nexists

2016-07-15 Thread Lars Hupel
> LaTeX build problems are not infrequent and could be avoided easily if > "build" produced the document by default. The quickest way to achieve that would be to set that in the ISABELLE_BUILD_OPTIONS environment variable in ~/.isabelle/etc/settings. Cheers Lars

Re: [isabelle-dev] \nexists

2016-07-15 Thread Lars Hupel
> It is unclear if and how we could get this platform zoo back: it was > rather accidental due to different administration regimes. OpenSUSE: Maybe. I can check how well my Ansible scripts work there, but no promises. Gentoo: Unlikely. macOS: Problematic because we currently have no appropriate

Re: [isabelle-dev] \nexists

2016-07-16 Thread Lars Hupel
> I am open to hear arguments why latex documents need to be continuously > available. So far there were none. That statement is unrelated to what you wrote afterwards, but let me give you an argument anyway: The generated PDFs are, as you probably agree, formal documents. In that sense, they

Re: [isabelle-dev] \nexists

2016-07-15 Thread Lars Hupel
> In contrast, a full "build -a" for the formal content is vital. The > shorter that takes, the more it becomes second nature to do it > frequently -- I often do it for every single changeset (before the local > commit). Not all of us have the appropriate hardware to do that. Speaking about TUM,

Re: [isabelle-dev] \nexists

2016-07-15 Thread Lars Hupel
Hi, > if you have the telemetry data you want to visualize, and just need a > tool for rendering them nicely, you can have a look at the tool I wrote > for GHC: > > GHC instance: https://perf.haskell.org/ghc/ > Tool website: https://github.com/nomeata/gipeda Gipeda does indeed look highly

Re: [isabelle-dev] Jenkins SPAM reduction

2016-07-16 Thread Lars Hupel
Glad you brought up this topic (although it isn't "spam" for any meaningful definition of "spam"). I wanted to do it anyway, because somebody asked me about it privately. > Jenkins sends lots of mails, and I find it hard to pay attention to them > at all. Even when I do look, the long message

Re: [isabelle-dev] \nexists

2016-07-18 Thread Lars Hupel
> Also the detailed parallel runtime parameters that are emitted every > 0.5s during a session running: number of active threads, pending futures > etc. How can I extract this information from within Isabelle/Scala? How would this information be presented? >> - What about sessions that grow in

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

2016-07-04 Thread Lars Hupel
> The problem I was referring to is that in order to get a deeper idea > what's going on you want to have a look at the topology of the history. > However I guess this is closely related to my surprise that not both > patches to distro and AFP pushed in proximity have been considered as > one

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

2016-07-04 Thread Lars Hupel
>> This is currently not implemented. Isabelle testboard will always use >> AFP devel and vice versa. It is not possible to test Isabelle testboard >> and AFP testboard together. > > But I regard this as a central use case: if a change to the distro > demands changes in the AFP, you want to test

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

2016-07-05 Thread Lars Hupel
> 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. Right, that's one

Re: [isabelle-dev] Build NEWS

2016-07-11 Thread Lars Hupel
>> I’m sure there are quite some papers which reference the /devel >> entries. > > I should hope not - they make no sense to cite, because their whole > purpose is to change on a daily basis. I'm with Gerwin here. In fact, the devel pages clearly state: "Please refer to release versions only in

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

2016-07-04 Thread Lars Hupel
To add to my last mail: > 3. Go to https://ci.isabelle.systems/jenkins/job/testboard-afp/ and > await new build run to be scheduled. There can currently only be one testboard build running at a time. That means you should wait to push until the previous run is finished. I understand that this

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

2016-07-06 Thread Lars Hupel
> What I see from this thread is that at some time we really have to talk > about official build orders with respective hg ids, either using > subrepos or whatever. That is accurate. So far we have largely avoided the need to do that, but with an ever growing AFP we need to figure out some

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle

2016-08-08 Thread Lars Hupel
> With a chart showing performance parameters (CPU time, elapsed time, > heap size) in the past few weeks, it should be normally easy to see a > small step or spike for HOL-Proofs or its applications. Happy to assist with that. In a previous mail you indicated that these parameters can be found

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

2016-07-02 Thread Lars Hupel
Hi Florian, thanks for your feedback! Commenting in some more detail will take me some time, but for now a quick reply: > 1. Changesets to dist and AFP exist as hg patches. This is currently not implemented. Isabelle testboard will always use AFP devel and vice versa. It is not possible to test

[isabelle-dev] Build failure in slow sessions

2017-02-22 Thread Lars Hupel
Dear developers, there have been some failures in the last two runs of the slow sessions: https://ci.isabelle.systems/jenkins/job/isabelle-nightly-slow/349/ https://ci.isabelle.systems/jenkins/job/isabelle-nightly-slow/348/ (Relevant changesets are listed there.) Unfortunately there have been

[isabelle-dev] Jenkins maintenance

2016-09-14 Thread Lars Hupel
Dear Isabelle developers, over the weekend, there will be – once again – a scheduled maintenance on the build infrastructure. I will add some more jobs (which are running nightly) to test a wider variety of side conditions (mainly -j/-o threads). I will take this opportunity to tidy up the

[isabelle-dev] Timeouts in AFP

2016-09-10 Thread Lars Hupel
Dear Isabelle developers, about yesterday, we experienced massive troubles in the automated AFP tests due to missing timeouts paired with sessions which don't terminate in current devel (after merging some new entries from AFP stable). I have added missing timeouts now in AFP/b60fb73dca31.

Re: [isabelle-dev] Jenkins maintenance

2016-10-05 Thread Lars Hupel
Thank you for bringing the discussion back on track. Let me try to address the remaining points. > I for one think that a big improvement would be a system where no one > pushes to the repository directly: every push goes to a testing server, > and if the test is successful, the changes can then

  1   2   3   >