Re: [isabelle-dev] Uses of Jenkins at TUM

> * My main use of Mira was to figure out which Isabelle version > corresponds to which AFP version, when something was broken in AFP. > > * I did not find this information in Jenkins, when I was still > spending more time on it last year. This information is all there. Build status is access

Re: [isabelle-dev] Uses of Jenkins at TUM

> In parallel (before and after Mira) we've had the older isatest. I don't > know if Mira ever had the ambition to replace isatest, but Jenkins tried > to do all that and failed. This was the start of my great worries about > the Isabelle administration and release infrastructure ... So, you're ju

Re: [isabelle-dev] Bad theory import "Main"

> This is still "blame game". If you say so. > I actually offered an open dialog about it last December, and you > rejected that. Because the offer consisted merely of rehashing things we already talked about in person. To be completely frank, I'm tired of repeating myself and others endlessly.

Re: [isabelle-dev] Bad theory import "Main"

> In the past 1.5 years, I've spent a lot of time trying to explain how > the Isabelle administration works. If we don't manage to overcome the > "blame game", things will decline further. You yourself proposed investigating Jenkins (then Hudson) some while ago, pointing out that e.g. the Scala te

Re: [isabelle-dev] Access problems to repositories and NFS

>> Indeed it is, thanks to the invaluable help of Franz Huber. However, he >> spoke of a workaround when he notified us and wasn't 100% certain it >> works reliably. I felt we should wait a few more days before we move the >> repo back, but I am easy either way. > > I would still suggest mainly pu

Re: [isabelle-dev] "No such file" in build

> For the moment it should work if you use an absolute path like -d > "$PWD/Lem". Yes, that works. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] "No such file" in build

I've just updated Isabelle (f3cd78ba687c) and am getting an odd error message for "isabelle build": *** No such file: "/home/lars/work/reify/verified-codegen/Lem/Lem/Lem_pervasives.thy" *** The error(s) above occurred for theory "Lem_pervasives" This is the invocation: isabelle build -bv -d Lem/

Re: [isabelle-dev] Access problems to repositories and NFS

> Indeed it is, thanks to the invaluable help of Franz Huber. However, he > spoke of a workaround when he notified us and wasn't 100% certain it > works reliably. I felt we should wait a few more days before we move the > repo back, but I am easy either way. I would still suggest mainly pushing to

Re: [isabelle-dev] Access problems to repositories and NFS

> Until the problems with lxbroy10 are resolved, please try lxbroy9 or > lxbroy8 as login nodes. The Isabelle repository should be available > there too. This appears to only give read access, not write access. In order to keep going with development, I've created a temporary clone on Bitbucket:

[isabelle-dev] Access problems to repositories and NFS

Dear Isabelle developers, since Thursday, there have been intermittent problems with access to our chair's servers; in particular, lxbroy10 which most people use to pull from/push to the Isabelle repository. The precise circumstances are unclear to me and not everybody seems to be affected. Unti

Re: [isabelle-dev] Fwd: Build of AFP entry Incompleteness failed

> A very weird error has somehow appeared That was due to my change in inductive. It's all resolved now. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Global constant names in inductive

> Your proposed change > https://isabelle.in.tum.de/repos/testboard/rev/20d5e446aa10 looks > formally OK. See now Isabelle/3c628937899d and AFP/a7160ffc25f1. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.

Re: [isabelle-dev] Global constant names in inductive

> Did you encounter an actual problem from that situation? > > Formally, a comment is not a problem. "Fixing" such things prematurely > is likely to break it. Yes, there is an actual problem. I define a function via "Function.add_function" and inspect the resulting info. As per usual discipline t

Re: [isabelle-dev] Global constant names in inductive

> I'm at a loss for an explanation. Does anybody have any idea what is > going on there? I now have an updated patch that instead of changing "add_inductive_global" to use "open_target"/"close_target" leaves it unchanged. With this, HOL-Proofs-Lambda and everything else goes through.

[isabelle-dev] Global constant names in inductive

Dear list, while poking around in the function package (to store more information in "info"), I also realized that I need a little bit more information from the inductive package. Reading its sources, I stumbled upon 10-year-old comments by Makarius that remind the reader of (what I assume is) no

Re: [isabelle-dev] SQLite-related error in testboard-afp job

> As with the old log files, any error to access the persistent data is > turned into a warning, since there might be old files still around, > while the logical data format has changed. > > > I don't know anything about testboard and can't say what is really going > on here. For whatever it's w

[isabelle-dev] Jenkins maintenance

Dear Isabelle developers, Jenkins will be unavailable tomorrow, April 5, from about 10:00 CEST to 12:00 CEST while our provider performs storage upgrades. Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu

[isabelle-dev] Avoid pollution of global code setup

long as the code setup is retained in all other places in the AFP (see attached patch). Before pushing this patch to the AFP I wanted to make sure that nobody else is affected by this change. Cheers Lars # HG changeset patch # User Lars Hupel # Date 1490094521 -3600 # Tue Mar 21 12:08

[isabelle-dev] Assertion error in Poly/ML 5.6

This is an assertion error from Poly/ML: poly: scanaddrs.cpp:218: void ScanAddress::ScanAddressesInRegion(PolyWord*, PolyWord*): Assertion `obj->ContainsNormalLengthWord()' failed. As far as I understand this is on Poly/ML 5.6 and nothing changed in the affected session. It may be spurious.

Re: [isabelle-dev] Build failure in slow sessions

> More now I have switched back to Poly/ML 5.6 (18f3d341f8c0), until I > find time to look what is really going on there. As a result the build is back on green. I think it's safe to assume that the Poly/ML upgrade is the culprit. Cheers Lars ___ isabel

[isabelle-dev] Build failure in slow sessions

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 n

Re: [isabelle-dev] Circular reasoning via multithreading seems too easy

> Tending global state (normally via Synchronized.var and not the raw > Unsynchronized.ref) has been part of the normal routine of Isabelle > maintenance in the last 10 years. At the beginning almost nothing > worked, but around 2008/2009 it became routine. Today we have a fairly > robust system, w

Re: [isabelle-dev] Circular reasoning via multithreading seems too easy

>> There are 48 occurrences of "Unsynchronized.ref" in "~~/src/Tools", 181 >> in "~~/src/HOL", and some more in the AFP (many of which appear to be in >> generated code). > > So what is wrong here? Nothing, as far as I am concerned. I was merely trying to answer your question. ___

Re: [isabelle-dev] Circular reasoning via multithreading seems too easy

> Where did you see these lots of Unsynchronized.ref (or better > Synchronized.var) in Isabelle Tools? There are 48 occurrences of "Unsynchronized.ref" in "~~/src/Tools", 181 in "~~/src/HOL", and some more in the AFP (many of which appear to be in generated code). _

Re: [isabelle-dev] AFP submission + Jenkins maintenance

> Everyone who considers submitting an AFP entry, please hold off until at > least November 12. We have been informed by the upstream provider about continued service disruption: "Unfortunately we encountered more difficulties than expected during the upgrade of the LRZ Cloud Computing infrastruc

[isabelle-dev] AFP submission + Jenkins maintenance

Dear Isabelle developers and users, our provider for some of our VMs has announced a scheduled maintenance, lasting from November 8 to November 11. The following parts of our infrastructure will be disrupted: - AFP submission service - "nightly slow" builds Since we're in the release phase anyw

Re: [isabelle-dev] Distro broken

Oh, nothing went wrong: Jenkins sent an email immediately after the push, and the status page also indicated the failure. Automation working as expected. Cheers Lars On 19 October 2016 11:11:21 CEST, Makarius wrote: >> Am Dienstag, den 18.10.2016, 20:40 +0200 schrieb Florian Haftmann: ***

Re: [isabelle-dev] Jenkins maintenance

> I had many private discussions with Lars in the past few months. I even > pointed out important requirements before the start of the Jenkins project. I am aware of that (I keep notes), and also of the relevant email threads dating back to 2014. > The present situation is that we have no proper

Re: [isabelle-dev] Jenkins maintenance

> I have often wondered how certain details are done by Jenkins, e.g. > logging into a remote machine, controlling the job and getting its results. Your use of the term "Isabelle/Jenkins" led me to believe that you're interested in the Ansible scripts. If you're instead interested in Jenkins sourc

Re: [isabelle-dev] Jenkins maintenance

> I have just used the new Jenkins testboard for the first time, and was a > bit disappointed by the very long runtimes: about 1.5h each for Isabelle > and AFP. This is slightly misleading, because the total time spent waiting for both is typically 1:30 hours; Jenkins runs them in parallel if poss

Re: [isabelle-dev] Jenkins maintenance

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 a

Re: [isabelle-dev] Fisher–Yates in AFP

> If it’s no problem, maybe the submission system could check for such > directories and delete them? I'm adding this to the list of additional checks (some are already in the works). I expect that the submission system will go through a maintenance period in the near future where this will get d

Re: [isabelle-dev] Fisher–Yates in AFP

> It isn’t only about SourceTree. As I mentioned, manually adding Fisher_Yates > had no effect, and even now "hg diff” shows nothing, even though Fisher_Yates > should appear as “added” or untracked (given that it’s on my machine and > nowhere else). I’ve also checked every .hgignore file. > >

Re: [isabelle-dev] Jenkins maintenance

> And where are the public sources of Isabelle/Jenkins? I feel like the other readers on this thread should know that you have asked me exactly the same question when you last visited Garching. I explained to you that some parts of the infrastructure cannot be public because they contain passwords

Re: [isabelle-dev] Jenkins maintenance

There are a lot of different issues in this thread, so let's unpack them separately. > Technical decisions need real reasons, not buzzwords. What's the buzzword? > It happens to very few people, only every 1-2 years. Such incidents are > not a problem and need not be taken into account of techni

Re: [isabelle-dev] Jenkins maintenance

> This reminds me of a still open question: Why is there this "continuous > integration" on every push anyway? This question is not open; it has been answered quite often in the past. For the repositories, it serves as a reminder to not push "broken" changes. (Or at least repair problems when the

Re: [isabelle-dev] Jenkins maintenance

> - This means that we're getting close to be able to run concurrent > jobs. Currently, some pushes don't get built: when a job is already > running and more than one push happens in the meantime (only the last > push is built). Soon, all pushes will get built. I will enable this for > the AFP re

Re: [isabelle-dev] Jenkins maintenance

(Please read carefully!) > 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] Jenkins maintenance

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 Jenkins

[isabelle-dev] Timeouts in AFP

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. There

Re: [isabelle-dev] Build statistics

> 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 s

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

> 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 in

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

> Is the test hardware in an air-conditioned server room? Of course. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] \nexists

>> 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

> 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 si

Re: [isabelle-dev] Build NEWS

> 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] Jenkins SPAM reduction

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 body

Re: [isabelle-dev] \nexists

> 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 need

Re: [isabelle-dev] \nexists

> 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, e

Re: [isabelle-dev] \nexists

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 releva

Re: [isabelle-dev] \nexists

> 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

> 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

> 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 observe

[isabelle-dev] Use HTTPS for components

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": -ISABELLE_COMPONENT_REPOS

Re: [isabelle-dev] Build NEWS

>> 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 c

[isabelle-dev] Build NEWS

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 the infrastructure and partly not my fault because the scripts to produce these pages make a lot of assumptions about the infrastructure :-) A

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

> 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 workflo

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. Right, that's one

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

> 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 buil

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

>> 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 t

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

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 is

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

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

Re: [isabelle-dev] AFP config files?

> 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 "thys/Catalan_Numbers/c

Re: [isabelle-dev] Jenkins maintenance

> 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 is

[isabelle-dev] Jenkins maintenance

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] Build NEWS

> * 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, push

Re: [isabelle-dev] Build NEWS

> 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 is

[isabelle-dev] Build NEWS

Dear Isabelle developers, this is an update about recent and upcoming changes in the build infrastructure. * Starting with Isabelle/e0513d6e4916 and AFP/e6727c33 I have moved the Jenkins build scripts into the Isabelle and AFP repository (they used to reside in a private "admin" repository).

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

> 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.

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

> 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

[isabelle-dev] Repaired Card_Equiv_Relations

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 ___ isabe

Re: [isabelle-dev] Isabelle repository broken

> 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 stat

Re: [isabelle-dev] Jenkins downtime

> 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 https://mailmanbroy

[isabelle-dev] Jenkins downtime

Dear list, the build services will be offline this weekend. I will perform some regular maintenance, but first and foremost I will flip on the mails again. isatest and afptest will be disabled for good. AFP maintainers (= people who have their mail address in a config file) might receive some spu

[isabelle-dev] Nonterminating AFP build

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 Randomised_

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

> 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 ma

[isabelle-dev] Remaining uses of isatest/afptest

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:*

Re: [isabelle-dev] Build NEWS

> * 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

Re: [isabelle-dev] Build NEWS

> 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

[isabelle-dev] Build NEWS

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 switc

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

> 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 https://mailmanbroy.informatik.tu-muenchen.de

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

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 isabelle.Options$.(options.scala:145)

[isabelle-dev] Failures in HOL-Codegenerator_Test

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 HO

Re: [isabelle-dev] Jenkins updates

> 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 mai

Re: [isabelle-dev] Jenkins updates

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

[isabelle-dev] Jenkins updates

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 discussions

[isabelle-dev] Disabled Jenkins mails

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 https://mailmanbroy.informatik.tu-muenchen.d

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

> 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, th

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

> 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.

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

> 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

> 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 memory.

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

>> 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 w

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

> 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 ho

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

> 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 ___ isabelle-de

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

> 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 https://mailmanbroy.informatik.tu-muenchen.de/

[isabelle-dev] Formula_Derivatives FAILED: Cannot allocate memory

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" ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.6-1/x86-li

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

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:

Re: [isabelle-dev] Jenkins maintenance window

> 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 happen

Re: [isabelle-dev] Jenkins maintenance window

> 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 t

[isabelle-dev] Jenkins maintenance window

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 kindl

<    1   2   3   >