ion system that is closer to old-school mailing lists
than real-time messenging
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
ces.
See also
https://isabelle-dev.sketis.net/phame/post/view/4/command-line_tool_isabelle_scala_project/
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
e general specification:
* plain and solid technology that solves more problems than it introduces
* self-hosted open-source platform (potentially a small company behind it)
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://
e closely at Discourse (more
than 10min so far).
Makarius
signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
t should be replaced eventually. This requires careful evaluation of
the underlying technology first.
The deeper question behind is: Can we re-unify our canonical forum of
discourse for Isabelle users? Or are we already subjects of big corporations
like Stackexchange, Zulip, Linked-In etc
On 27/11/2019 20:00, Makarius wrote:
> On 27/11/2019 19:20, Clemens Ballarin wrote:
>> While doing 'isabelle build -a', macOS 10.14.4 (Mojave) informs me that
>> 'csdp' is a 32-bit executable that won't run on Catalina [1]. This is
>> for revision c9433e8e314e of yesterday.
er of certain options in "Security &
Privacy". Applications that request certain rights, but are rejected in the
first attempt, should show up in various dialogs. E.g. see "General" (as in
https://isabelle.in.tum.de/img/macos_security.png or "Privacy" with &quo
On 02/03/2020 17:39, Makarius wrote:
> This is an update on the Isabelle2020 release process.
>
> * Isabelle2020-RC2 is to be expected within 1-2 weeks: this will be also the
> fork-point for the Isabelle release repository
> https://isabelle.sketis.net/repos/isabelle-release
T
w amended that here:
changeset: 71553:cf2406e654cf
tag: tip
user:wenzelm
date:Sat Mar 14 21:58:29 2020 +0100
files: src/Pure/thm.ML
description:
more robust: proper transfer if Context.eq_thy_id;
Thus it also fits better to Thm.join_transf
derstands which parts and discuss proposed changes with that person. The
Mercurial history often provides some clues about that, but you can also just
ask on the mailing list.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://
On 15/03/2020 13:05, Makarius wrote:
> I am in the process to publish Isabelle2020-RC2: changeset 7eadccd4392c.
>
> This will be also the fork point for the isabelle-release vs. isabelle-dev
> repositories.
>
> Please refrain from pushing anything to isabelle-dev until a ch
On 10/03/2020 15:02, Makarius wrote:
> On 02/03/2020 17:39, Makarius wrote:
>> This is an update on the Isabelle2020 release process.
>>
>> * Isabelle2020-RC2 is to be expected within 1-2 weeks: this will be also
>> the
>> fork-point for the Isa
r something that will be fairly
> lightly used however.
So why not put it into some library theory somewhere?
There is no need to change the presentation of the core logic, just for
another variant of quantifiers.
Makarius
___
acter, leading to popup).
Note that for a few years already, we have had a trend to replace old ASCII
notation by proper Isabelle symbols (while keeping remains of it in input
methods).
* Fill the free space of "!" by Georgy's proposal with Larry's name for it.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
for universal quantification.
With a tiny little bit of effort we could have a version of "isabelle update"
that replaces all remaining uses of "!" automatically.
That would be a contribution to ecology and health of features.
Makarius
__
ls" panel, in group "Abbrevs", which is the
first one that is open by default.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
various sub-languages belong to the isabelle-users mailing list.
Over there we can also discuss what you are trying to do and how Isabelle can
be used for that.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman
Ubuntu 18.04 (TeXlive) and failed on macOS (macTeX). Could
> be due to outdated LaTeX packages.
Which version of macTeX is this actually?
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
great
> to compare it with Isabelle's.
You should ask this on the isabelle-users mailing list; isabelle-dev is for
developing Isabelle itself, not Isabelle-based tools.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https:
On 03/10/2020 16:43, Makarius wrote:
> Here is an intermediate report on the state of support for the ARM64 platform,
> according to Isabelle/694d0a315d0a.
>
> Presently, its main hardware representative is my new Raspberry Pi 4B (4 CPU
> cores at 1.5 GHz, 8 GB RAM), running Ubu
be + AFP/ff20b0ab160b successfully on macOS
10.14.6 with the regular MacTeX-2020 download from https://tug.org/mactex
(clicking on the app and letting the installer do its job).
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
On 19/10/2020 17:34, Makarius wrote:
> *** HOL ***
>
> * An updated version of the veriT solver is now included as Isabelle
> component. It can be used in the "smt" proof method via "smt (verit)" or
> via "declare [[smt_solver = verit]]" in the cont
, and have
lost the connection to people out there people out there who were trying to
use these interfaces.)
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
ers. Due to some new "isabelle build_XYZ" tools this is getting more and
more robust and reproducibly, on an increasing number of platforms:
arm64-linux already works for many things (even though it is strictly speaking
a toy right now).
Makarius
_
running "-o
document=pdf" more often than normal, just to make double sure.
In the second phase, I used the visual diffpdf tool on Ubuntu, but only for
the entries in $ISABELLE_HOME/src/Doc.
Do you have more tricks and techniques to share?
auto_nitpick enabled.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
On 27/09/2020 21:26, Makarius wrote:
>
> This refers to Isabelle/684f14b1e7fc (and AFP/35158287da0b).
>
> At the Isabelle Workshop 2020, Clemens Ballarin proposed to switch to LuaLaTeX
> by default: it allows advanced packages programmed in the Lua scripting
> language.
One
On 25/08/2020 22:06, Makarius wrote:
> *** HOL ***
>
> * Nitpick/Kodkod may be invoked directly within the running
> Isabelle/Scala session (instead of an external Java process): this
> improves reactivity and saves resources. This experimental feature is
> guarded by system op
ut my own TODO list, but would definitely like
to add a few things to Isabelle/jEdit, e.g. integrated support for repository
browsing.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
ews to produce a
proper code generator for Poly/ML eventually. People who have some ideas
should contact me or David via private mail.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
On 03/10/2020 16:43, Makarius wrote:
> Here is an intermediate report on the state of support for the ARM64 platform,
> according to Isabelle/694d0a315d0a.
>
> Presently, its main hardware representative is my new Raspberry Pi 4B (4 CPU
> cores at 1.5 GHz, 8 GB RAM), running Ubu
suitable GUI presentation, e.g. a “tag cloud”
instead
of an old-fashioned directory tree.
"""
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
).
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
. in the past 12
months. It might be due to subtle changes in how parallel proofs and proof
terms are managed. I am in the process to investigate it further: luckily
there is a mostly reproducible situation on a Mac Mini provided by EPFL.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
-deterministic game.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Thu Aug 06 23:44:43 2020 +0200
files: src/Pure/Tools/build.scala
description:
recovered stderr for PIDE batch-build, such as "Browser info at ...",
"Document at ..." (see also 940195fbb282, 5469bacf5573, 5c4800f6b25a);
Note that option -v is not
On 11/08/2020 17:00, Makarius wrote:
> On 09/08/2020 20:28, Makarius wrote:
>> On 09/08/2020 19:55, Lawrence Paulson wrote:
>>> What on Earth is this?
>>>
>>>> 17:40:59 Loading theory "Nullstellensatz.Nullstellensatz_Field"
>>>> 17:40:
me, 0.000s GC time
>> 17:40:59 *** exception Fail raised (line 683 of "statistics.cpp"): No
>> statistics available
I guess it is a situation that David Matthews has described to me privately:
$HOME/.polyml is somehow filled up and should be
nswering threads is as follows (high to low):
1. isabelle-dev
2. isabelle-users
3. isabelle-dev material that does not belong here
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
ust old.
Answer to the original question: see the "implementation" manual section "0.2.4
Printing ML values" (with examples).
(These questions belong to the isabelle-users mailing list, where more people
can benefit from the answers as well.)
Makarius
___
far from being proofs in pure
> lambda calculus, but they are a good starting point for postprocessing, and I
> think it is more important that they are minimal and computationally efficient
> to create given the context.
I find this all very interesting
of memory
resources, and potentially avoid exhausting them too early.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
On 03/08/2020 13:33, Makarius wrote:
> On 01/08/2020 13:24, Tobias Nipkow wrote:
>> I suspect that is not of your making. Poly/ML, OS and even the hardware come
>> to mind...
>>
>> On 01/08/2020 11:15, Lawrence Paulson wrote:
>>> Run #347 (with one s
On 04/08/2020 12:46, Lawrence Paulson wrote:
> I could do this quite easily on my nice big work machine, but it’s really not
> practical on a laptop. I hope we can get the testboard working again soon.
> Larry
>
>> On 4 Aug 2020, at 11:39, Makarius wrote:
>>
>&g
On 09/08/2020 20:28, Makarius wrote:
> On 09/08/2020 19:55, Lawrence Paulson wrote:
>> What on Earth is this?
>>
>>> 17:40:59 Loading theory "Nullstellensatz.Nullstellensatz_Field"
>>> 17:40:59 ### theory "Nullstellensatz.Nullstellensatz_Field"
threads?
> I would appreciate if you can have a look at it.
I still need to revisit a few pending aspects of this seemingly trivial
upgrade of isabelle build.
Makarius
signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
abelle-dev.sketis.net/rPOLYMLfb10196d998b --- the HOL4 guys
had observed genuine crashes.
So for now, lets continue with the assumption that things work smoothly again.
Makarius
signature.asc
Description: OpenPGP digital signature
___
isab
isabelle.systems/jenkins/job/isabelle-all/2078/
I have also seen this, especially on some macOS machines.
The update to polyml-5.8.1-20200708 does not have any effect on it.
So this particular problem is still open.
Makarius
___
isabelle
lle/ML.
It is still possible to opt-out, e.g. like this "isabelle build -o
pide_session=false", but at a later stage non-PIDE batch builds will be
discontinued.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https
ften working with -Xmx30g on big machines, but not higher: there is a
32/64 discontinuity beyond 32 GB.
Makarius
signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
On 19/06/2020 11:36, Makarius wrote:
> On 19/06/2020 07:41, Florian Haftmann wrote:
>>
>> I guess this »java.lang.OutOfMemoryError: Java heap space« is due to
>
> In recent years, JVM resource limitations have become more and more difficult
> to circumvent. The proble
On 06/06/2020 11:01, Tobias Nipkow wrote:
>
>
> On 05/06/2020 13:43, Lawrence Paulson wrote:
>>> On 5 Jun 2020, at 12:29, Makarius wrote:
>>>
>>> HOL-ex has always been an odd bin for very mixed material. I don't see a
>>> reason to delete that:
On 08/06/2020 15:51, Lawrence Paulson wrote:
>> On 8 Jun 2020, at 14:20, Makarius wrote:
>>
>> Larry, are you going to add HOL-Examples yourself? Otherwise I will do it
>> later today.
>>
>> I have already done it for Pure-Examples (material stemming from
&g
>> On 31 May 2020, at 22:52, Makarius wrote:
>>> Conceivably it could be subdivided, as it seems to have 94 entries.
>>
>> Now might be actually a good time to disallow sub-directories of a session
>> directory. They have accumulated a lot of confusion and proble
pec has a corresponding theory in "$L4V_ARCH/" that contains the
> platform-dependent part of the formalisation which is included in the generic
> part.
I don't quite understand this. Can you point to the actual source?
Does it mean you dynamically change t
ed a problem, because the underlying image would
become a bit slower and bigger. Now we have fewer uses of HOL-Library as
parent image, instead the few required theories are included/reloaded via
"'sessions' HOL-Library".
Makari
On 04/06/2020 11:42, Lawrence Paulson wrote:
>> On 3 Jun 2020, at 20:30, Makarius wrote:
>>
>> So you were proposing multiple sessions, like we have already with
>> HOL-Induct,
>> HOL-Isar_Examples?
>
> I don’t understand this point. For b
an opportunity to test it, and provide feedback on time.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
ttps://isabelle-dev.sketis.net/rISABELLE9c0b835d4cc2
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
elle.in.tum.de/website-Isabelle2021-RC2/dist/index.html
My impression is that the webserver at TUM is in a bad state (again), but the
content of the underlying file-system looks good.
I will tell the local admins.
Makarius
___
isabelle-dev ma
, at least
until the end of the Christmas season (10-Jan-2021).
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
T36
If there are further Big Sur problems, we should at least collect them properly.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
difier "CS"
overrides this: then all defining and referencing positions are shown.
See also option "jedit_focus_modifier".
This refers to Isabelle/f7954a960890.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https
my own servers running: 2 Jitsi-Meet and 1 BigBlueButton, and
ran some small sessions quite successfully in the past few weeks.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
is only a small part of the actual TODO list for the release, but it
might help in overall communication and coordination.
(I don't want to spend to much time on publicly visible activity, or rather
"agility" just to look cool.)
Makarius
___
-m100 HOL
isabelle log -U -m100 -v -T HOL.Set -T HOL.Nat HOL
(Technically this is based on PIDE markup + messages produced in batch-mode. I
will see what else can be done with it on the spot for the release.)
Makarius
___
isabelle-dev mailing lis
t.
> Since the ML file is dependent on syntax that is independently introduced by
> those theories, I'm unsure how to fix this. The naive solution would be to
> duplicate the ML file, but that seems inelegant.
Duplication is even worse.
Makarius
___
On 23/12/2020 15:56, Makarius wrote:
> On 23/12/2020 10:08, Lars Hupel wrote:
>>
>> Based on my superficial understanding, this problem appears to be caused by
>> two different theories including the same ML file
>> (src/HOL/Hoare/hoare_syntax.ML).
>
> There is
xample call in the code
How is this related to the Isabelle development process?
You should ask this on the isabelle-users mailing list.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
On 05/11/2020 17:04, Fabian Huch wrote:
> unused_thms reporting thms that are not unused does seem strange to me.
I will come back to this soon (presently diverging into other old mails).
Makarius
___
isabelle-dev mailing list
isabe
sible to import old Mailman histories into
the system under consideration?
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
e has
become a scarce resource.)
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
On 03/11/2020 20:57, Makarius wrote:
>
> I never see Zulip, though, and this explains my wording of "walled garden" or
> "walled site".
>
> BUT: the Lean community has this public archive generated from the hidden
> garden: https://leanprover-community.
er experience reports on either system (or even
something else).
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Just a quick reaction to a problem at TUM on Sunday evening:
https://isabelle-dev.sketis.net/rISABELLE97f12d2c8bf2c735c02f63728855c63e8d12b9ee
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman
ions for user feedback in the
coming Isabelle release process, using the existing service
https://bbb.augsburg.one ...
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
that should be avoided.
Such a profound change of how Isabelle works needs good justifications. And
afterwards it usually takes years to get such a change through.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tu
rather profound in
Isabelle.
The treatment of unnamed facts in particular is also fairly canonical
concerning our own standards.
Can you say what is wrong with this, and why it needs to be "improved"?
Makarius
___
isabelle-
ot;Tag: provers".
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
stage, I should probably merge ideas from
"$ISABELLE_HOME/src/Doc/antiquote_setup.ML" back into more official
antiquotations in Isabelle/Pure.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
On 27/12/2020 20:23, Makarius wrote:
> We are in an early stage of the official Isabelle2021 release process.
>
> The blog https://isabelle-dev.sketis.net/phame/blog/view/2 and the workboard
> https://isabelle-dev.sketis.net/project/board/4 provide a clue where we are.
&g
On 08/01/2021 16:10, Manuel Eberl wrote:
> I have a small amount of material for HOL-Data_Structures and for
> Algebraic_numbers in the AFP. Will put that in in the next day or two.
OK, just tell me when you are finished.
Ma
), macOS (visual glitches).
Existing Isabelle installations (repository closes etc.) need to change
Utilities / Global Options / Appearance / Swing look & feel to "FlatLaf
Light", or "FlatLaf Dark" (presently untested).
Makarius
On 08/01/2021 14:11, Makarius wrote:
> On 27/12/2020 20:23, Makarius wrote:
>> We are in an early stage of the official Isabelle2021 release process.
>>
>> The blog https://isabelle-dev.sketis.net/phame/blog/view/2 and the workboard
>> https://isabelle-dev.sketis.net/pro
the keyword + PIDE rendering colors: for Isabelle/VSCode
I've made only very crude setup some years ago.
I think some users already have a slightly better private setup.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman
On 10/01/2021 12:32, Makarius wrote:
>
> It looks like we are ready. I will make the release fork later today, within
> approx. 4h.
The post-release point is now
https://isabelle.sketis.net/repos/isabelle/rev/1105c42722dc
This means that everything pushed onto the isabelle-dev r
On 09/01/2021 01:25, Makarius wrote:
> *** Isabelle/jEdit Prover IDE ***
>
> * Improved GUI look-and-feel: the portable and scalable FlatLightLaf is
> used by default on all platforms (appearance similar to IntelliJ IDEA).
>
> This refers to Isabelle/efc58b56a6c7, it avoids va
t is to sprinkle "isabelle jedit -b" generously into various
build scripts.
Next time, I could just make Isabelle/jEdit an integral part of
Isabelle/Scala: like Isabelle/VSCode and other add-ons are already today.
Makarius
___
isabelle-
far: Netcup
GmbH in Kaiserslautern.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
in adopting current Scala.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
te that I did manage to build Isabelle + AFP with pdf + HTML several times
on other big machines, using settings like this:
ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms1g -Xmx8g -Xss16m"
ML_PLATFORM="x86_64_32-linux"
ML_OPTIONS="--minheap 1500"
M
itable change soon.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
-- it often shows up as landing page for
systematic web search of questions and answers.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
On 02/01/2021 12:07, Makarius wrote:
> On 02/01/2021 10:03, Lars Hupel wrote:
>>> In Isabelle/38528017e4c8 there is some more verbosity, to see where it gets
>>> stuck --- if it is repeatable at all.
>>
>> It still gets stuck.
>
> I have managed to repro
arious "bugs" coming
from it eventually.
Makarius
On 05/06/2020 03:51, Klein, Gerwin (Data61, Kensington NSW) wrote:
>
>
>> On 4 Jun 2020, at 03:44, Makarius wrote:
>>
>> On 01/06/2020 02:54, Klein, Gerwin (Data61, Kensington NSW) wrote:
>>>
>
ean for compatibility, both backwards and forwards.
Eventually we shall see other document formats than PDF, e.g. based on HTML or
PreTeXt (formerly MathBook XML).
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
right now. A regular parallel session crashes like
this:
exception Fail raised (line 506 of "profiling.cpp"): Profiling is currently
active
(I need to ask David Matthews about it: a few years ago parallel profiling did
work to some extent.)
Makarius
ack as a symlink, the
canonical /p/home/isabelle-repository might be more robust (after other
changes in the future).
After a bit of further consolidation, I expect fewer problems with lxbroy10 in
the future than we've had in the past. (Gentoo often caused strange problems
that nobody understood.)
On 02/06/2021 20:30, Makarius wrote:
> On 02/06/2021 16:57, Lawrence Paulson wrote:
>> I’m getting error messages (see below). Any news?
>
> lxbroy10 has been reinstalled: instead of an unusual Gentoo setup it is now
> Ubuntu 20.04; moreover the NFS directory layout has bec
101 - 200 of 407 matches
Mail list logo
