unused_thms reporting thms that are not unused does seem strange to me.
Fabian
On 05/11/2020 16:39, Fabian Huch wrote:
unnamed facts at the top level of a theory (i.e., unnamed lemmas or theorems)
don't work smoothly with the rest of Isabelle.
I see three possible ways to do improve
Hi,
unnamed facts at the top level of a theory (i.e., unnamed lemmas or
theorems) don't work smoothly with the rest of Isabelle.
For instance:
- they appear nowhere in the theory exports (naively, one could think
they appear as literal facts)
- unused_thms ignores them and thus will
To clarify: that was only about the testboard repository. The other
repositories had a problem earlier today when accessed from
isabelle-repository, but do work again.
Fabian
On 6/2/21 5:21 PM, Fabian Huch wrote:
Our directory structure has changed slightly, and it appears that the
directory
Our directory structure has changed slightly, and it appears that the
directory was a Symlink that is now dead.
I'll make sure that the testboard is restored but that may take until
Friday.
Fabian
On 6/2/21 4:57 PM, Lawrence Paulson wrote:
I’m getting error messages (see below). Any news?
It is now possible for Isabelle developers to start and stop builds on
the jenkins [1].
To log in, use your ldap credentials for our tum-servers, i.e. the
account you use to push to the isabelle/isabelle-server.in.tum.de
repositories.
Also, the testboard job can now be parameterized with an
You probably need to initialize the user settings first with "isabelle
components -I" if it's a new machine.
Fabian
On 3/12/21 1:34 PM, Peter Lammich wrote:
On Fri, 2021-03-12 at 13:24 +0100, Manuel Eberl wrote:
Have you done the usual "isabelle components -a"?
I would like to, but it has
There seems to be a performance degradation in the presentation
somewhere between Isabelle/adb10e840b71 and Isabelle/2b212c8138a. I
notified Makarius about that but didn't spot the error yet (there were
lots of changes in the signature).
I think the jenkins build should be configured to send
On 11/16/21 10:08, Gerwin Klein wrote:
On 16 Nov 2021, at 7:41 pm, Gerwin Klein wrote:
On 16 Nov 2021, at 7:37 pm, Fabian Huch wrote:
On 11/16/21 09:16, Gerwin Klein wrote:
You were too fast :-), afp-devel is is for isabelle-devel, it
shouldn't have isabelle-release changes
On 11/16/21 09:16, Gerwin Klein wrote:
You were too fast :-), afp-devel is is for isabelle-devel, it shouldn't have
isabelle-release changes in it.
It's unfortunate that isabelle-release has already diverged in content. Not a
real problem, just a bit more overhead.
Ok, so I'll make an
On 2/2/22 14:33, Martin Desharnais wrote:
Dear Isabelle developers,
I don't know who is responsible, but the web interface to testboard
[1] (or other CI projects for that matter) seems to be down.
Thanks for letting us know. The Jenkins master node crashed, but is now
back online.
Thanks, the jenkins process crashed -- this technology is getting less
and less reliable.
Fabian
On 9/10/23 10:43, Lawrence Paulson wrote:
… is out of action again, the website at least
Larry
___
isabelle-dev mailing list
isabelle-...@in.tum.de
o here, please let me know.
Cheers,
Julian
On Mon, Sep 26, 2022 at 10:18 AM Fabian Huch wrote:
Dear maintainers,
the entries "Buchi_Complementation" and "PAC_Checker" both fail to
build since Sep 17. You might not have been properly informed as the
initial failure was
The function package produces a duplicate simp rule in some
circumstances. MWE:
fun a :: "bool ⇒ bool ⇒ bool ⇒ bool" where
"a True True _ = True" |
"a False True False = True" |
"a True _ True = True" |
"a _ _ _ = False"
Creates the warning:
Ignoring duplicate
From Jenkins, the tighter interval is Isabelle/3fb2c47a7605 ..
Isabelle/1a9decb8bfbc [1,2].
Fabian
[1]: https://ci.isabelle.systems/jenkins/job/isabelle-all/4411/
[2]: https://ci.isabelle.systems/jenkins/job/isabelle-all/4412/
On 4/17/23 14:49, Makarius wrote:
We have a problem with
Builds depend very much on the implicit state of their predecessor -
sessions that were previously built and are still consistent with the
current sources are skipped.
If you go a few builds back, the output is 42,927 lines.
Fabian
On 7/12/23 11:09, Lawrence Paulson wrote:
I was testing
n 12 Jul 2023, at 11:58, Fabian Huch wrote:
Builds depend very much on the implicit state of their predecessor - sessions
that were previously built and are still consistent with the current sources
are skipped.
If you go a few builds back, the
In the following minimal example:
datatype t = A | B "t × t"
fun f :: "t ⇒ bool" where
"f A ⟷ True"
| "f _ ⟷ False"
quickcheck throws an error if you invoke it (both Isabelle2022 and
latest devel):
lemma "f x = True" quickcheck
Does anyone have an idea what's going on? The error is as
I just encountered a theory that wouldn't terminate with threads=1, but
does so with more threads. The reason was a left-over `try` - which
obviously might not terminate, but with more than a single thread, the
rest of the session is checked, whereas with a single thread, it never
progresses
On 2/29/24 10:38, Makarius wrote:
An odd (unexplained) change has occurred on AFP:
changeset: 14197:ddf90847bfa5
user: immler
date: Tue Feb 27 15:10:13 2024 +0100
files: thys/Ordinary_Differential_Equations/Ex/Lorenz/C1/Lorenz_C1.thy
thys/Ordinary_Differential_Equations/ROOT
Trying twice works as the heap images generated in the first run can be
re-used.
Also I have bumped the time-out to 400 minutes, but such a waiting time
is ridiculous -- we are working hard on a distributed build system,
which will bring down build times to a tolerable level again.
Fabian
On 3/19/24 19:37, Makarius wrote:
On 19/03/2024 13:21, Fabian Huch wrote:
Today marks 20 years of AFP -- to celebrate, here are a few timings
with the new parallel build (Isabelle/08b83f91a1b2 and
AFP/b61f72e5cba6):
build -a
0:08:47 elapsed time, 3:02:23 cpu time, factor 20.75
build -A: -X
Today marks 20 years of AFP -- to celebrate, here are a few timings with
the new parallel build (Isabelle/08b83f91a1b2 and AFP/b61f72e5cba6):
build -a
0:08:47 elapsed time, 3:02:23 cpu time, factor 20.75
build -A: -X slow -a
0:43:11 elapsed time, 72:49:01 cpu time, factor 101.17
build -A: -a
! Is this what the testboard uses now? And I can't quite figure
out what these three runs represent.
Larry
On 19 Mar 2024, at 12:21, Fabian Huch wrote:
Today marks 20 years of AFP -- to celebrate, here are a few timings with the
new parallel build (Isabelle/08b83f91a1b2 and AFP/b61f72e5cba6
On 3/27/24 23:01, Makarius wrote:
So while Jenkins is running (How many hours? Without stop button?)
Side note: there is a stop (and start) button if you log in to the
Jenkins using your TUM credentials.
Fabian
___
isabelle-dev mailing list
The Jenkins regularly chokes (likely due to bad programming and
unmaintained plugins). The high system load also has the effect that the
isa-afp page can get slow sometimes.
We'll replace it soon: A prototype of the new build system is available at
https://build.proof.cit.tum.de
Fabian
On
On 5/10/24 17:44, Tobias Nipkow wrote:
On 10/05/2024 09:35, Fabian Huch wrote:
The Jenkins regularly chokes (likely due to bad programming and
unmaintained plugins). The high system load also has the effect that
the isa-afp page can get slow sometimes.
Very slow to the point of being
26 matches
Mail list logo
