Re: [isabelle-dev] ADTs in Scala

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

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

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

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

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

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

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?

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

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

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

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

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

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

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

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

> 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

(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] Future of isatest/afptest

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

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

> 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

> 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

(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

> 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

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

> 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

> 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

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

> 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

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] Grouping ISABELLE_FULL_TEST?

> 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

> 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

> 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

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

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

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

> 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] Maintenance work on Jenkins VM

> 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

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

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

> 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

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?

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?

> 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

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

> 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

> 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

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

> 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

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

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

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 ___

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

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

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

[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

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

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

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

[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

[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

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

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

[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

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

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

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

[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

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

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

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

> 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

> 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

> 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

> 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

> 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

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

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

> 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

> 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

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

> 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

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

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

> 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

> 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

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

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

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

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

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

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

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

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

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

(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

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

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

  1   2   3   >