ssh-clone at
https://isabelle.sketis.net/repos that is updated every 10 minutes.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
On 21/03/2019 15:22, Makarius wrote:
>
> Note that there are many implicit dependencies of OPAM, notably
> libgmp-dev for zarith. Thus it can be difficult to use "isabelle
> ocaml_setup" on macOS. And I did not fully succeed on Windows/Cygwin yet.
After all I manag
le2019 for sorting out inevitable problems coming from
that.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
tc/settings somehow
fit to that.
You can shuffle jdk components in local settings like this:
init_component "$HOME/.isabelle/contrib/jdk-8u181"
init_component "$HOME/.isabelle/contrib/jdk-11"
This jdk-11 is the OpenJDK from Oracle. We are now using a different one
from https://adoptopenjdk.n
bundle, to get more modular ways to
enable/disable the syntax locally.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
2018, you could run "hg bisect" to
find the problem in the history. This will be a bit time-consuming, though.
Note that you need to run "isabelle components -a" and a strict
"isabelle jedit -b -f" in every step.
Makarius
___
isabel
lities for stateless generated /
exported files for the Isabelle2019. If anything is still missing or not
properly working, we have still a few weeks to sort it out.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman
On 06/04/2019 14:04, Lars Hupel wrote:
>
> Scala 2.13.0-RC1 has just been released:
>
> <https://downloads.lightbend.com/scala/2.13.0-RC1/scala-2.13.0-RC1.tgz>
>
> Maybe Makarius could package this as an Isabelle component already.
>
> Scala 2.13.1 i
s:
init_component "$HOME/.isabelle/contrib/scala-2.12.6"
or to whatever other version you see fit.
End-users won't have to build Isabelle/Scala anyway: a release provides
finished Isabelle/Scala/jEdit jars.
Makarius
___
isabelle-dev ma
a
scala> val afp = AFP.init(Options.init())
scala> afp.entries_map("Buchi_Complementation").maintainers
Of course it is also possible to inspect the file AFP/metadata/metadata
manually, but the above opens many possibilties for Isabelle/Scala
system programming.
Makarius
019 release the main goal is to
polish the programming interfaces to make it all work smoothly -- such
that there are no remaining reasons to write physical files into the
session source space.
Makarius
___
isabelle-dev mailing list
isabelle-...@
ss an argument, then an error is raised
>> because the list of arguments is empty.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
On 30/03/2019 21:16, Makarius wrote:
> On 30/03/2019 20:00, Julian Brunner wrote:
>>
>> At the moment, the executable merely complements a hardcoded automaton
>> and writes it to a file for testing and benchmarking purposes. It will
>> not stay like this. Once a parser f
On 30/03/2019 00:22, Makarius wrote:
>
> Current examples are in AFP/09ea4594dc4e:
>
> * Diophantine_Eqns_Lin_Hom for Haskell (with GHC)
Thanks to the truly portable Haskell Stack, this works even on Windows
(Isabelle/c17c654f6bb6 + AFP/a8142ac5e4b6).
For example:
$ isabelle
On 21/03/2019 16:12, Makarius wrote:
> On 21/03/2019 16:08, Makarius wrote:
>> On 21/03/2019 16:02, Lars Hupel wrote:
>>>> * Update to OPAM 2.0.3: this is the latest version, and the one that
>>>> the current Cygwin 3.0.4 provides.
>>>
>>&
On 21/03/2019 16:08, Makarius wrote:
> On 21/03/2019 16:02, Lars Hupel wrote:
>>> * Update to OPAM 2.0.3: this is the latest version, and the one that
>>> the current Cygwin 3.0.4 provides.
>>
>> This broke idempotency (or maybe something else?):
>>
o the build will have to stay red for a
> while, much to the disadvantage of people who rely on it.
BTW, on Ubuntu 18.04 the most basic way is to install the ocaml and
libzarith-ocaml packages, and put this into etc/settings:
ISABELLE_OCAMLFIND="
On 06/04/2019 20:09, Makarius wrote:
>
>> Instead of bisect, I took an educated guess after looking at the file
>> history of Admin/components/main. So the first bad commit for me is
>> b578749daa62 (which introduces scala 2.12.8). With its parent isabelle jedit
>> -
default. It is derived from etc/preferences
ML_system_64=false (x86_64_32), or true (x86_64).
> ML_SYSTEM="polyml-5.7.1”
We are at polyml-5.8, but you should not change ML_SYSTEM here. Just
omit that item.
Makarius
___
isabelle-dev m
.
Could there be a situation where the "exhaustive" tester produces really
large lists (millions of entries) and then runs in stack-overflow due to
the recursive Generated_Code.map function?
Makarius
theory Scratch
imports Main
begin
declare [[quickcheck_fi
Somehow the archive of this mailing list stopped working recently, e.g.
see
https://mailman46.in.tum.de/pipermail/isabelle-dev/2019-April/thread.html
where I get less than 20 messages, mostly by myself.
Who is actually the administrator for the mailing list?
Makarius
lusion: OpenJDK 11 is more honest in the rendering, i.e.
a good display gives good results, a bad display gives bad results.
I will work on the text of the manual later: with updated notes about
high-quality vs. low-quality displays; also about font hinting vs.
non-hinting.
mma'). This is a subtle change
of semantics wrt. old-style %name.
This refers to Isabelle/d13865c21e36, it is a refinement of the new
marker concept to accomodate HOL-Analysis better -- I have already
updated its tags to the new format in Isabelle/f0
rns out that something is printed after all, but the first column
> is missing.
Maybe it is just a matter of Page Setup / Paper size. The default
appears to be Letter: switching it to A4 works for me and that becomes
persistent (I don't know where this information is st
On 31/05/2019 17:33, Makarius wrote:
> On 31/05/2019 14:26, Tobias Nipkow wrote:
>> In 8dd987397e31, when I try to print (Cmd-P) I get
>>
>> "An error occurred while trying to print: Invalid print service"
>
> Over the years, I have occasionally seen such an
On 31/05/2019 19:48, Tobias Nipkow wrote:
>
>> It works fine, after making sure that the paper format is A4.
>
> I don't understand. Where do I "make sure"?
In the printer dialog, but you said that you it does not show up a
On 15.06.19 21:27, Yuri wrote:
On 2019-06-15 11:58, Makarius wrote:
All sources are included, but such "hobby packaging" as I call it is
not going to work. Isabelle is very complex. It is not something you
disintegrate and reintegrate without loosing a lot.
But what do you sugges
is.
Nobody has a benefit from bad re-packaging of Isabelle. We have seen
this in the past several times. There is no point to repeat the
experiment: the result will be the same.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
ongoing post-release
development, and applied to only one of the two repository
branches.
* isabelle-users is the place to discuss Isabelle2019-RC
versions.
* isabelle-dev is the place to discuss ongoing post-release
development
On 13/05/2019 15:16, Fabian Immler wrote:
>
> @Makarius: Could you please add the attached exported changeset to
> isabelle-release?
> Otherwise I'll push the change to isabelle-dev.
OK, I will add it to isabelle-release. Note that the proper mailing list
for isabelle-release is is
else is for the isabelle-users mailing list:
"[it] provides a forum for Isabelle users to discuss problems,
exchange information, and make announcements."
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
gnoring some of the drop-outs.
These Java guys are so conservative that it will probably take 10 more
years to get this right, maybe when X11 will be discontinued altogether.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
sic Analysis
C full Analysis with Homology etc.
D HOL-ODE etc.
For the funny letters see https://en.wikipedia.org/wiki/AAA_battery --
it merely illustrates the idea, and is not meant literally.
Makarius
___
isabelle-dev mailing list
isa
finished by then.
Then there will be 6 weeks for final polishing + an optional 7th week.
Afterwards I will be on travel, so this is a fixed timetable for the
release train.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://
not expect any problems from not being at "latest" scala-2.12.8 --
these are marginal maintenance releases on a fairly stable branch.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
belle/Scala
invoking Poly/ML. The images are relocatable as usual.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
On 08/04/2019 18:15, Lars Hupel wrote:
>
> Maybe Makarius could change that behaviour and instead of "build"
> refusing to build anything, only exclude malformed sessions.
Such a total existence failure of the session graph is hard to pin down:
it would require adhoc rearrang
On 09/04/2019 12:09, Lawrence Paulson wrote:
> Thanks. What about a single entry?
>
> isabelle build -d '$AFP' Groebner_Bases
> *** Undefined Isabelle environment variable: "AFP"
>
>> On 9 Apr 2019, at 10:59, Makarius wrote:
>>
>> # almost all of Is
ivation management (eventually with full export of
dependencies, as well as proofterms -- at least for "small" sessions
like HOL-Analysis; right now even Main HOL still causes problems).
Makarius
theory Test
imports FOL
begin
ML \Proofterm.proofs := 1\ (*adhoc change at run
and elitist
Isabelle environment.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
On 23/08/2019 22:35, Makarius wrote:
>
> https://github.com/phacility/phabricator
The blurb says "Open software engineering platform and fun adventure
game" and indeed it is: the authors have an odd sense of humor (e.g. in
the documentation), but the overall product is quite im
tion is so good, in contrast to e.g.
the average Github project.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
On 22/08/2019 23:12, Lars Hupel wrote:
>
> It would behove you to stop discrediting me by using ALL CAPS and
> calling the valid points I'm bringing up "noisy".
This thread was meant for technical discussions about better Mercurial
hosting infrastructure.
On 20/08/2019 21:52, Makarius wrote:
> https://bitbucket.org/blog/sunsetting-mercurial-support-in-bitbucket?utm_source=alert-email_medium=email_campaign=bitbucket-eol-mercurial_EML-5301=104256548=749141674
That text is typical marketing talk. Someone else has been very quick in
answer
ing releases and events like the
Mercurial conference in Paris May-2019. (I've come by the conference via
the presentation
https://heptapod.net/download/Heptapod-2019-paris-hg-conf.pdf).
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum
actually found it via that list.
I also like this other entry: https://www.versionshelf.com with the
slogan "Saving you and your team from distraction." But its hosting
platform is probably non-open-source.
Makarius
___
isabelle-dev
shrinking considerably. An you would
have to look closely to find a good hosting platform.
Right now, if a git user asked me about hosting, I would point to
phabricator.org (which is for SVN, Mercurial, Git) :-)
(But I do need a bit more experience with it so say something
definitely. I will set
know
> what it would do with git branches, and for such repositories I use git
> directly.
I usually use git directly when working with colleagues on git projects.
My preferred front-end is VSCode: it hides a lot of the "coolness" of git.
Makarius
ify the overall setup.
It would be great if this is not a reason for divorcing Isabelle from
AFP at the bottom of SCM technology. Such a split would mean that I had
to spend more resources to work around it -- resources that are better
invested elsewhere.
Makarius
___
nd of the
dialogue. Ultimately, I want to help them improve the overall quality of
their software project -- we cannot carry the full weight of ITP users
alone.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
On 22/08/2019 23:05, Makarius wrote:
>
> To get more repository infrastructure, my research at that time ended
> at Phabricator by Phacility, see https://www.phacility.com/phabricator
>
> Despite strange product/company name, this looks fairly good at first
> sight. It is an o
On 23/08/2019 21:59, Makarius wrote:
>
> Here is an example Phabricator installation, which happens to be for the
> Mercurial project itself: https://phab.mercurial-scm.org/diffusion/HG/
Another example is Phabricator development hosted by Phabricator itself:
https://secure.phabri
* preferably self-hosting, on standard virtual machines
* good culture, good manners, good style
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
market-based decisions.
What counts for "tooling" is Isabelle itself: it is non-standard and
self-hosting in many respects. We have been quite successful with that
approach in the past decades.
I am aware of the user-management problem. There must be proper
sol
On 12/09/2019 16:04, Christian Sternagel wrote:
>
> On 9/12/19 3:04 PM, Makarius wrote:
>> *** General ***
>>
>> * Session ROOT files need to specify explicit 'directories' for import
>> of theory files. Directories cannot be shared by different sessions.
>>
d than ever before, and the
overall session/theory management has become more robust and faster.
The scheme turned out a bit more liberal than I anticipated some years
ago: it is still possible to have multiple directories for a single
session, even though t
problems.
This unclear situation in AFP was the main reason why we had to suffered
2 years with increasingly slow PIDE startup times.
I am glad that it has turned out so well in current AFP/98320942654a.
Makarius
___
isabelle-dev mailing list
is
On 12/09/2019 15:04, Makarius wrote:
> *** General ***
>
> * Session ROOT files need to specify explicit 'directories' for import
> of theory files. Directories cannot be shared by different sessions.
> (Recall that import of theories from other sessions works via
> session-qual
On 12/09/2019 16:04, Christian Sternagel wrote:
>
> On 9/12/19 3:04 PM, Makarius wrote:
>> *** General ***
>>
>> * Session ROOT files need to specify explicit 'directories' for import
>> of theory files. Directories cannot be shared by different sessions.
>>
On 12/09/2019 20:32, Makarius wrote:
>
> Whenever I pass by this JNF-AFP-Lib session, I wonder if there is any
> remaining use of it. It quotes a lot of theories without a check if they
> are actually needed. Loading the material takes only 30s in my 8core
> machine.
Here ar
a better way to achieve the same goal without creating
> superfluous ad-hoc sessions?
One could try to make this systematic via Isabelle/Scala, similar to
option "isabelle jedit -R" -- but it requires to look very closely what
is really required.
Makarius
__
accumulated features. Afterwards it should be sufficiently
clear to make it work easily on Windows again.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
On 16/09/2019 21:00, Makarius wrote:
>
> This needs further work on my side. I am presently in the process to
> throw out accumulated features. Afterwards it should be sufficiently
> clear to make it work easily on Windows again.
See now Isabelle/b3f61e166763, which stack
us.
> BTW. what's the difference between isabelle-repository and isabelle-dev?
These "project tags" have their own description. I am still in the
process to figure out how this should be arranged. Whatever happens, I
will try to keep the descriptions up-to-date.
Maka
On 25/09/2019 21:58, Makarius wrote:
> Our new Phabricator service for Isabelle development is taking shape:
> https://phabricator.sketis.net
The URL is now https://isabelle-dev.sketis.net
Makarius
___
isabelle-dev mailing list
is
isabelle-users mailing list: most of the time
there is actually a misunderstanding about the need to change internals.
This is also the deeper reason why there is no "issue tracker" for
Isabelle users: it is usually just a matter of an open discussion to do
things properly.
On 26/09/2019 15:31, Makarius wrote:
>> But now (Isabelle/ffbe7784cc85 and AFP/66bfe59e1850) this has stopped
> working. I get a red squiggly line under the import of
> "Concurrent_Revisions.Operational_Semantics" in "Foo".
it will become possible to push changes to hosted
repositories, and thus getting rid of other hosting services like
Bitbucket or Github eventually.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
ite (e.g. https://isabelle.in.tum.de) explains the
purposes of the mailing lists. (The cookbook is outdated/misleading in
many other respects.)
Makarius
signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@
was rather minimal, because the text is
rather implicit about the important detail of session directory management.
After the reform it generally becomes simpler and faster, so there is
even less to say about it. Main point: session ROOT entries need to be
explicit about extra directories.
On 25/09/2019 21:58, Makarius wrote:
> Our new Phabricator service for Isabelle development is taking shape:
> https://phabricator.sketis.net
>
> The platform provides many Apps to support software development, but so
> far I have focused on the key things, like repository h
ent to force a fresh build, e.g. with option -c or -f.
In rare situations one needs to remove the bad database file manually.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
On 12/11/2019 21:36, Makarius wrote:
>
> Isabelle/c073c4e79518 already has some "isabelle phabricator" tools for
> that, even with documentation in the "system" manual.
>
> A few practically important things are still missing:
>
> * automated ssh se
On 25/10/2019 14:29, Makarius wrote:
>
> To help anybody interested in independent hosting (of SVN, Mercurial,
> Git) and to minimize my own administrative workload, I intend to provide
> a few Isabelle/Phabricator tools in Isabelle/Scala within the next few
> weeks (Feb-2019
On 03/12/2019 21:16, Makarius wrote:
> On 03/12/2019 19:34, Manuel Eberl wrote:
>>
>> On another probably unrelated note, whenever I open a theory with a lot
>> of dependencies in Isabelle/jEdit (e.g. HOL-Analysis.Analysis with only
>> the HOL image loaded), the ent
(no UI reaction to clicks etc). The theory panel is also
> still blank at that point (except for the "Analysis" theory).
This is unrelated. I am presently bisecting the history to find out where it
occurs first.
Makarius
___
isabel
UM, and both hardware nodes are available. On this machine the
standard quasi-interactive build is rather fast and stable:
Isabelle/d411d5c84a4b
ML_PLATFORM="x86_64_32-linux"
ML_HOME="/home/makarius/.isabelle/contrib/polyml-5.8.1-20191124/x86_64_32-linux"
ML_SYSTEM="polyml-5.
NEWS blog at https://isabelle-dev.sketis.net -- with automated propagation to
the isabelle-dev mailing list.
See also
https://isabelle-dev.sketis.net/phame/post/view/1/isabelle_phabricator_setup
(Actually, mailing list propagation does not quite work yet, so I pasted this
to copy repositories with some of there meta-data).
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
will formalize these Phabricator configuration tweaks in Scala as
"isabelle phabricator_setup".
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
nd Windows. The macOS executable that we ship with csdp-6.x is an
older version.
Before that we were using CSDP as "software as a service" over the Net,
but that was very slow and unstable.
Makarius
___
isabelle-dev mailing list
isabelle-
It is clear that such things need to be updated eventually. The standard
scheme is to have everything working with Catalina with the next official
Isabelle release.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
On 28/11/2019 15:06, Makarius wrote:
> In other words: users who want to use Isabelle2019 with everything as expected
> need to stay away from the macOS update.
>
> It is clear that such things need to be updated eventually. The standard
> scheme is to have everything workin
ssible to build on such ancient versions. In that case one
needs to rethink the situation.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
uses extra problems.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
On 28/11/2019 16:21, Lawrence Paulson wrote:
>> On 28 Nov 2019, at 14:06, Makarius wrote:
>>
>> users who want to use Isabelle2019 with everything as expected
>> need to stay away from the macOS update.
>>
>> It is clear that such things need to be update
tch queue mode that
has become popular again recently under the slogan of "CI" -- it requires lots
of tinkering and experimentation due to lack of proper interaction with the
machine. (Or maybe the CSDP provider wants to make such a setup for his
project.)
to recycle old TUM-style login names: Phabricator can map names
found in commits to its own user naming scheme. For example, my own
entry is "makarius (Makarius Wenzel)" instead of "wenzelm".
Eventually, there will be more and more explanations within Phabricator
itself, e.g.
On 25/09/2019 21:58, Makarius wrote:
> Our new Phabricator service for Isabelle development is taking shape:
> https://phabricator.sketis.net
>
> The platform provides many Apps to support software development, but so
> far I have focused on the key things, like repository h
urial, Git,
Subversion.
Some co-authors already got email invitations for it -- it is not publicly
visible. On request, I can provide further hints about such self-hosting --
apart from what is documented in the "system" manual chapter 6.
Makarius
On 19/12/2019 20:52, Makarius wrote:
> *** System ***
>
> * The command-line tool "isabelle hg_setup" simplifies the setup of
> Mercurial repositories, with hosting via Phabricator or SSH file server
> access.
Another note on the implementation: it uses the Phabri
On 10/02/2020 21:05, Makarius wrote:
>
> Looking briefly through the calendar, we can probably make it in the 6 weeks
> from 01-Mar-2020 (Isabelle2020-RC1) to 15-Apr-2020 (Isabelle2020 final).
>
>
> Are there other side-conditions? E.g. pending things that need to get
being lost in the
great cleansing.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
y watch every
day just for fun.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
s to avoid the "Stickiness of Siren Servers" in the
terminology of Jaron Lanier, "Who owns the future?", 2013.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
On 10/02/2020 21:05, Makarius wrote:
>
> Looking briefly through the calendar, we can probably make it in the 6 weeks
> from 01-Mar-2020 (Isabelle2020-RC1) to 15-Apr-2020 (Isabelle2020 final).
>
> Are there other side-conditions? E.g. pending things that need to get int
nts emerge only for the user who
invokes the tool.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
description:
ignore generated dependency files (see 91d5a8255c98, fd5cd1daf6a9);
This also belongs to the gradle/IntelliJ project setup for
Isabelle/Scala ("isabelle scala_project").
Makarius
___
isabelle-dev mailing lis
On 10/02/2020 22:51, Makarius wrote:
> On 10/02/2020 21:05, Makarius wrote:
>
> Now is also a good time to check what has been done recently, and fill it into
> NEWS and CONTRIBUTORS.
>
> (We have overall relatively little to say this time, because I have spent so
> mu
lle development workshops" many years ago.
If anybody has ideas how to repeat that (including funding), I am keen discuss
it. E.g. via private mail, or directly in Paris at IJCAR 2020 and the Isabelle
Workshop 2020.
Makarius
--- Begin Message ---
Hi everyone,
This is a reminder that
1 - 100 of 407 matches
Mail list logo
