On 10/10/17 20:50, Makarius wrote:
>
> import isabelle._
>
> val options = Options.init
> val afp = AFP.init(options)
>
> isabelle.graphview.Graph_File.write(options +
> "graphview_font_size=24", Path.explode("afp.pdf").file,
> afp.entri
On 10/10/17 20:50, Makarius wrote:
> The above change to AFP is required to avoid cyclic dependency of
> Jordan_Normal_Form vs. Polynomial_Factorization, due to session JNF-AFP-Lib.
>
> This problem can be exhibited as follows (without the change):
>
> Exn.capture { af
ot; takes "condition" options with the
corresponding environment values into account, when determining the
up-to-date status of a session.
This is the updated situation according to Isabelle/be08a7691c62.
Makarius
___
isabelle-dev maili
mplex situation of auxiliary sessions in AFP.
Makarius
# HG changeset patch
# User wenzelm
# Date 1507659422 -7200
# Tue Oct 10 20:17:02 2017 +0200
# Node ID e65225a319b03ff627d67f7d68459937409f03d2
# Parent cd292cbedcb9cfe65f9aee2f44fb639bf13b3fa2
avoid cyclic dependency of Jordan_
On 08/10/17 17:03, Christian Weinz wrote:
>
> Isabelles pdflatex document build fails when there is a space or any of
> ä, ö, ü, ß and % in a theories name. Possibly more characters are
> affected.
Why not post this on the isabelle-users mailing list?
On 06/10/17 16:38, Makarius wrote:
>
> Presently (e.g. in Isabelle/0b3fa8e22f22) this causes a new problem with
> OCaml, see also my thread on the Cygwin mailing list:
> https://cygwin.com/ml/cygwin/2017-10/msg00037.html
>
> $ ocaml nums.cma
> Cannot load required s
*** Prover IDE -- Isabelle/Scala/jEdit ***
* Completion supports theory header imports.
This refers to Isabelle/f27488f47a47.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman
f OCaml on Cygwin64 really is.
Maybe some OCaml expert can say more about it.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Please ignore this -- wrong address.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Hallo Jens,
wie sieht es diese Woche mit Mittagessen aus? Bei mir ginge Do und Fr,
jeweils 13:00.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
useful in general, and
we can probably discontunue some existing session group tags, e.g. "ZF"
or even "AFP".
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
$ISABELLE_HOME/etc/settings:
init_component "$HOME/.isabelle/contrib/polyml-test-e7a662f8f9c4"
That is useful for testing, but also for using the ML compiler 5.7,
which provides PIDE markup for scopes of bound variables.
Makarius
___
is
shortcut. E.g. a
proper re-build with all heaps could fail due to resource or timing
problems.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
principle possible to re-implement that as native
x86_64-linux and still use short 32bit addresses for ML).
Note that with Ubuntu 17.10, Canonical slowly starts to phase out 32bit
hardware support. This is not immediately relevant for us, but it shows
that things are changing.
Makarius
Cygwin that is bundled with the Isabelle
Windows application, e.g. from
http://isabelle.in.tum.de/devel/release_snapshot (when it is updated
itself after 30-Sep-2017).
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https
/ML).
Some Isabelle components still need to be updated (e.g. for Sledgehammer).
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
o Isabelle/4c98c929a12a. It means that after the
Isabelle2017 everything becomes really serious about qualified theory
names, e.g. session images no longer affect the theory name space.
It will eventually have further impact on isabelle build.
.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
r library concepts and pushed that
through all applications in AFP.
We should see better times pretty soon: I've started to rework the build
process right now.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
, too.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
isabelle-release repository. I am myself
mentally back to isabelle-dev.
* The situation of afp-devel is still somewhat unclear to me. When will
the fork to afp-2017 happen?
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https
after some weeks; but it is
better to publish changes now than to stockpile them for a long time.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On 08/09/17 11:13, Makarius wrote:
> The all-important release fork will happen today in the evening.
That is now!
Within the next hour there should not be any pushes to
http://isabelle.in.tum.de/repos/isabelle in order to avoid confusion
about the two branches.
I will come back a bit la
On 03/09/17 12:06, Makarius wrote:
>
> The isabelle-dev repository remains open for 3 more days. Afterwards it
> forks to https://bitbucket.org/isabelle_project/isabelle-release and
> further changes (really important ones!) need to be sent to me via email.
There were some delays, bu
tail in
which order the sessions are built, and where are wait-times with unused
CPU cores.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
h there are sometimes old habits to overcome as usual.
You can also try http://isabelle.in.tum.de/website-Isabelle2017-RC1 with
its fresh environment.
Makarius
signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isa
On 21/08/17 20:24, Makarius wrote:
>
> The first official release candidate Isabelle2017-RC1 is anticipated for
> 2/3-Sep-2017, that is a bit less than 2 weeks from now.
>
> That is also the deadline for any significant additions.
That is today. I will publish Isabelle2017-R
e.in.tum.de/repos/isabelle/annotate/fc41a5650fb1/src/HOL/ROOT#l75
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
builds and fastest build times ever,
and throwing even more cores at it could improve it without further ado.
Makarius
Isabelle/19bf4d5966dc
AFP/419b0f1b9088
ML_PLATFORM="x86-linux"
ML_HOME="/home
ar:
everything *must* be imported as qualified afterwards.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On 30/08/17 21:50, Makarius wrote:
> On 30/08/17 09:21, Tobias Nipkow wrote:
> I still need to investigate the details, but it is probably just a very
> long failed attempt to find the hg root.
I have now improved that as follows:
changeset: 66558:37b16f8af351
tag:
thing: the Prover IDE potentially needs to edit
everything, so all sessions with their theories need to be explored
beforehand.
This is apt to become a problem on Windows or on a networked file-system.
Makarius
___
isabelle-dev mailing list
isabel
t a very
long failed attempt to find the hg root.
Is this actually a networked file-system, or anything else that is
somehow special?
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
) to make
small additions and do some fine tuning.
After the Isabelle2017-RC1 there will be the usual 4-6 weeks to sort out
genuine problems only, notably ones that have been newly introduced
since the last release.
Makarius
signature.asc
Description: OpenPGP digital
RC1, but
it also depends a lot on the participation of users testing the RC chain.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
show up, it is time to finish and not to start new things.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
updated the important files NEWS, CONTRIBUTORS, ANNOUNCE
in Isabelle/5c0a3f63057d, but it seems that many potential entries are
still missing.
Please provide entries in NEWS and CONTRIBUTORS for all relevant things
you have done since the last release.
Makarius
lit of the plugin in Isabelle/9098c36abd1a.
A possible application is to change the logic session image and then
stop/start the Isabelle plugin (but *not* the Isabelle Base plugin).
At some point there might be an official action / menu for that, if it
turns out sufficiently important.
On 19/08/17 21:27, Makarius wrote:
> I propose to try the previous Scala release locally, e.g. as follows in
> $ISABELLE_HOME_USER/etc/settings:
>
> init_component "$HOME/.isabelle/contrib/scala-2.12.2"
Do not forget "isabelle jedit -b -f" after flipping Scal
evious Scala release locally, e.g. as follows in
$ISABELLE_HOME_USER/etc/settings:
init_component "$HOME/.isabelle/contrib/scala-2.12.2"
If that crashes again, we can be quite sure that it is jdk-8u144.
Makarius
___
isabelle-de
bout the system? Hardware, OS etc.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
13)
* hardware: AMD Ryzen 7 1800X Eight-Core Processor
I've seen occasional press articles discussing problems of AMD Ryzen,
e.g.
https://www.phoronix.com/scan.php?page=news_item&px=Ryzen-Compiler-Issues
Makarius
__
-f
> Log attached
This refers to a separate log file
/home/manuel/hg/afp-devel/hs_err_pid13339.log
If you still have that, can you send it to me?
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.
onger used.
Here is the result for AFP (Isabelle/158c513a39f5 and AFP/0a57dd7e945a),
using the following command-line:
isabelle imports -M -d '~~/src/Benchmarks' -d '$AFP' -a
unused file
"/home/makarius/isabelle/repos/AFP/thys/Berlekamp_Zassenhaus/Tests.thy"
unused
adhoc sessions with
overlapping sources.
Hopefully it now works smoothly. In any case, the coming weeks before
the Isabelle2017 release are there to consolidate it beyond doubt.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https
cades, but I have
changed that recently into into "sort_by" to make it coincide with the
terminology of the Scala library.
See
http://isabelle.in.tum.de/repos/isabelle/rev/610794dff23c
Makarius
___
isabelle-dev mailing list
isabelle-...@in.t
As of Isabelle/96ad7d5ff613 we are on current scala-2.12.3, see also
http://scala-lang.org/news/2.12.3
The changeset ensures a full rebuild of all Isabelle/ML and
Isabelle/Scala, to avoid surprises we've seen in past Scala updates.
Mak
-3839149.html
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
t;headless PIDE" interaction under program control.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On 11/08/17 22:59, Makarius wrote:
>
> Poly/ML 5.7 does not work for Isabelle
>
> In the meantime, David Matthews has revised many things, so it probably
> works again, but it needs systematic testing on all platforms and
> 32/64bit combinations.
I have made some experiment
revised many things, so it probably
works again, but it needs systematic testing on all platforms and
32/64bit combinations.
I have presently no idea about release plans of Poly/ML 5.7.x. Anything
for Isabelle2017 needs to happen within the next 4-6
significant changes is
actually 6 weeks before the final lift-off, i.e. at the point where the
fork of isabelle-dev and isabelle-release repositories happens.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https
cation. I still need to figure out how this works in the first
place ...
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
for extra
confusion of names in a theory, but proper name space operations are
better than simulating that with 'notation' / 'no_notation'. (Alphabetic
syntax tokens should be kept at a minimum anyway: they are subtracted
from the identifier syntax category.)
Makarius
___
/df85956228c2. These are fully localized
commands, in contrast to the very old-fashioned hide_const, hide_type etc.
Maybe this occasionally helps to sort out name space confusion, although
it is probably a feature of last resort.
Makarius
___
isab
rect ISABELLE_HOME directory.
You've also said that your VSCode is from the OS package repository.
Maybe it is better to use the official
https://code.visualstudio.com/Download
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
On 02/07/17 13:31, Christian Sternagel wrote:
> On 07/01/2017 09:21 PM, Makarius Wenzel wrote:
>> There is also a "State" panel that imitates the dockable of the same
>> name in Isabelle/jEdit. You will get to that via the "isabelle.state"
>> command, e.g
ls. Although, this poses the problem of
multi-window management.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
he application:
presently it lacks the all-inclusive application bundling of Isabelle/jEdit.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
use SML_import to access these in
strict SML, e.g. see src/Tools/SML/Examples.thy (which is also available
in the Documentation panel).
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On 24/06/17 21:08, Florian Haftmann wrote:
> See now finally http://isabelle.in.tum.de/repos/isabelle/rev/a41435469559
Great. In Isabelle/d91108ba9474 we are also back to scala-2.12.2 and can
hopefully keep it this time.
Makarius
signature.asc
Description: OpenPGP digital signat
niences at the
BigProof event in Cambridge, where I am attending from 10..27-Jul-2017.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
also
taken into account by the regular scalac maintainers eventually?
Alternatively, if Florian has an idea for a workaround it is also fine.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On 19/06/17 14:16, Makarius wrote:
> On 19/06/17 13:38, Lars Hupel wrote:
>
>> - I just unpacked the attachment you sent and, with scalac 2.12.2 I get
>> a "StackOverflowError" (in the patmat phase), before I even got a chance
>> at running this
>
> I h
and ran into a confusion of
SCALA_HOME. Maybe this is the actual cause of the problem. I will
investigate further ...
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
ROOT.scala
*** At command "export_code" (line 18 of
"~~/src/HOL/Codegenerator_Test/Generate.thy")
Attached is the generated source.
Makarius
test.scala.xz
Description: application/xz
signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
a
change in the Poly/ML repository.
Since we did not have that for the huge Iptables_Semantics_Examples last
year, we ran blindly into the unpleasant surprise of a Poly/ML 5.7
version that no longer worked for us.
Makarius
___
isabelle-de
tthews gets a proper test session
Iptables_Semantics_Examples1 and we routinely see its results in
http://isabelle.in.tum.de/devel/build_status
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On 22/05/17 15:16, Makarius wrote:
> On 22/05/17 13:12, Lars Hupel wrote:
>>> After your change d76937b773d9, I still see a non-terminating
>>> HOL-Codegenerator_Test. So in 94b0da1b242e I have switched back to
>>> scala-2.11.8.
>>
>> Interesting. In J
e.systems/jenkins/job/isabelle-repo-makeall/912/consoleFull>.
> (I had tested it with testboard before anyway.)
>
OK, I will look more closely again.
There are some other problems with Windows: some of this already works
in e896db33d4ce, but it
2.11.8.
I have also improved http://isabelle.in.tum.de/devel/build_status/ to
show failed sessions on the main page, so that I will see such problems
earlier next time.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mail
With Isabelle/a43a079156a6 we are on scala-2.12.2, leaving the 2.11.x
behind.
This is a major update, in particular it makes better use of the
underlying Java 8 platform.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On 15/05/17 14:33, Makarius wrote:
> On 15/05/17 12:14, Makarius wrote:
>> Some results can be seen here:
>>
>> http://isabelle.in.tum.de/devel/build_status/Poly_ML_5.7_Linux/index.html
>> http://isabelle.in.tum.de/devel/build_status/Poly_ML_5.7_Linux_2_threads/index.h
PIDE can edit any source
file you like and know to which session it belongs.
Further fine points might still need polishing. I hope we manage that
during the summer, such that it all works smoothly for the Isabelle2017
release.
Makarius
__
red as an Isabelle
> component in my "etc/settings"
See
http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg07321.html
Quote:
In current Isabelle/6acb28e5ba41 it is also possible to use something
like "isabelle jedit -R -l MY_SESSION" to restr
it shows that simple things can be done in a simple way,
without too much boilerplate of JDBC. Moreover, I did not pull in any of
the more ambitious Scala/JDBC projects that are emerging elsewhere.
Makarius
___
isabelle-dev mailing list
isabelle
On 15/05/17 14:24, Makarius wrote:
> On 15/05/17 12:29, Lawrence Paulson wrote:
>> Version 5.7 doesn’t even build on my main workstation, though it works
>> on my MacBook Pro running broadly similar software. No idea what is
>> going on here, but I’m not happy about it.
>
On 15/05/17 12:14, Makarius wrote:
> Some results can be seen here:
>
> http://isabelle.in.tum.de/devel/build_status/Poly_ML_5.7_Linux/index.html
> http://isabelle.in.tum.de/devel/build_status/Poly_ML_5.7_Linux_2_threads/index.html
>
> The test hardware is similar or actually
atable on all these platform variations.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
quot;Generated at Tue, 18 Apr 2017 00:02:04 GMT").
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
trib/polyml-5.7"
$ isabelle components -a
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
lit the theory into Factorial and Binomial,
>> to raise awareness of existing combinatorial material in HOL.
>
> See now bdd17b18e103.
>
> Theory Pre_Main is still present, but now trivial to get rid of.
Great. I've done that now in 3039d4aa7143.
M
essing it all up.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
erformance measurements.
There is more in the data that is not plotted yet, e.g. the precise
relation of tests run with threads=1,2,4,6. Or online heap usage, thread
activity, future tasks, etc. for an individual process (ml_statistics).
At last we are no longer "flying blind" ...
On 24/04/17 14:46, Makarius wrote:
> This is another attempt to open a discussion about Jenkins at TUM.
Thanks to everyone who participated on this thread. I have learned a few
new things, which I will pick up again soon.
Makar
arbitrary entry point
http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg06783.html
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On 24/04/17 14:46, Makarius wrote:
>
> Are there users of it outside the TUM group?
>
> What is good about it? What is bad about it?
(1) To follow the line of Mira vs. Jenkins:
* My main use of Mira was to figure out which Isabelle version
corresponds to which AFP version, when s
ation and release infrastructure ...
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
the
situation in AFP -- it should be possible to make one big sweep with
"isabelle imports -U" to have qualified theory imports everywhere. That
will be also the point of no return, but there is no need to rush into that.
Makarius
___
isab
plex_Main"
should be imported from the HOL session, not anything in between. (This
is a concession to the complex bootstrap process of HOL.)
In Isabelle/85ed070017b7 Florian has already improved the imports of GCD
further.
Are there good ideas how to do it with Binomial? Thus we could get rid
ows that in "blame game" mode it is hard to communicate in a plain
and simple way.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On 24/04/17 14:36, Makarius wrote:
> On 23/04/17 18:10, Blanchette, J.C. wrote:
>>
>> *** No such file:
>> "/Users/blanchette/isabelle/src/HOL/Library/Fraction_Field.thy"
>> *** The error(s) above occurred for theory "HOL-Lib.Fraction_Field" (line 17
time believing that you're
> willing to engage in constructive dialog about regression testing anymore.
>
> You claim that you "did not get any answers". In reality, you got all
> the answers and ignored them.
This is still "blame game".
I actually offered an
This is another attempt to open a discussion about Jenkins at TUM.
Are there users of it outside the TUM group?
What is good about it? What is bad about it?
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https
oth -- there can be intermediate situations, where certain sessions
cannot import certain theories anymore.
The emerging tool "isabelle imports" tools helps to sort out the
situation, but it requires some care to use it and I am still exploring
the overall situati
t 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.
Makarius
___
isabelle-dev mailing li
it would be interesting to discuss some basic things. What is
good about it? What is bad about it?
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
e might be errors
from all_known = true (ae09b9f5980b);
This means you should see some "Java vomit" on the terminal at startup
of Isabelle/jEdit, as well as some text popup with a half-decent error
message. Plugin startup is always a bit fragile.
Makarius
__
On 22/04/17 19:34, Blanchette, J.C. wrote:
>
>> On 22.04.2017, at 19:17, Makarius wrote:
>>
>>> scala> PIDE.resources.session_base.known.files.toList.find(p =>
>>> p._2.exists(_.theory == "M
301 - 400 of 2785 matches
Mail list logo
