evil in some sense.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
e merely disabled Isabelle OPAM and OCaml as follows
in $ISABELLE_HOME_USER/etc/settings:
ISABELLE_OPAM_ROOT=""
ISABELLE_OCAML=""
ISABELLE_OCAMLC=""
That is rather brutal, but allows me to continue with the current tip
version.
Makarius
ve had this discussion some
month ago concerning stack: it is just too heavy to be the only way to
refer to ghc).
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
l
case.
Another remaining application of full x86_64 is the huge PIDE session
forked by "isabelle dump" and related tools: it can require 64GB
(excluding slow), and I have not explored the upper end yet.
Makarius
___
isabelle-dev mailin
On 13/03/2019 21:12, Makarius wrote:
> On 13/03/2019 21:00, Florian Haftmann wrote:
>> Am 13.03.19 um 20:57 schrieb Lars Hupel:
>>>> isabelle ocaml_opam install zarith
>>>
>>> This should ideally happen on-the-fly from within Isabelle/ML.
>>
>>
m
Export/Generated_Files in ML for the 'codegen' command in particular.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
at the
beginning of May. It all should be finalized an published until
15-Jun-2019, when I will go on travel (not vacation, but a visit to
colleagues in Paris).
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu
NCOMPATIBILITY in command-line syntax.
This refers to Isabelle/cc0b3e177b49.
Short version: "isabelle build -s" is now "isabelle build -o
system_heaps", and various other command-lines have been simplified. It
is also possible to provide system_heaps via etc/pref
ion.add_locale_cmd including any assumptions we defined in ML.
Isabelle/ML belongs to the normal Isabelle user space, so isabelle-users
is the place to go.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informa
On 22/02/2019 22:59, Makarius wrote:
> On 22/02/2019 16:47, Manuel Eberl wrote:
>> I came upon a regrssion with the position information in terms that
>> contain calligraphic or Fraktur letters, e.g.:
>>
>> theory Scratch
>> imports Pure
>> b
nt to break the persistent data model just to be fully
up-to-date at the "tip" version.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
o
>>
>> define G where "G = homology_group 0 (subtopology (nsphere 0) {pp})"
It might be better to introduce a proof-local version of 'abbreviation'.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.in
icode standard than the
calligraphc "M". E.g. see these results in Console / BeanShell or
Console / Scala:
> "풜".length()
2
> "ℳ".length()
1
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
ely see (1) happening really soon: the
"isabelle update" tool belongs to certain newly introduced
infrastructure that deserves proper consolidation. (It is time to start
thinking about which already open threads should be closed for the release.)
Makarius
much less resources).
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
to be
tested thoroughly, of course.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On 16/02/2019 14:07, Florian Haftmann wrote:
> Am 14.02.19 um 13:34 schrieb Makarius:
>>
>> In contrast to my proposal concerning Flyspeck-Tame-Base it is better to
>> keep the main AFP document unchanged, e.g. like this:
>>
>> session Flyspeck-Tame
e it is better to
keep the main AFP document unchanged, e.g. like this:
session Flyspeck-Tame-Eval (very_slow) = Flyspeck-Tame + ...
This will change the timing for Flyspeck-Tame in the recorded database,
but such renamings occasionally happen over the years.
Makarius
_
aybe it is possible to make a non-slow session "Flyspeck-Tame-Base"
that does everything except the actual "eval" steps, and postpone the
checks to session Flyspeck-Tame (very_slow) = Flyspeck-Tame-Base ...
Makarius
On 10/02/2019 19:47, Makarius wrote:
> I have fine-tuned the Isabelle DejaVu fonts in
> Isabelle/4791988fcbc4 to impose the FreeType auto-hinting beforehand to
> the TrueType file: this leads to isabelle_fonts-20190210 in
> Isabelle/7e5a7a11d5d1.
>
> In summary:
>
> *
On 10/02/2019 20:12, Makarius wrote:
> On 10/02/2019 20:08, Peter Lammich wrote:
>> No luck on my machine. The font rendering still looks slightly
>> blurred.
>>
>> However, I'm using an old Linux (Ubuntu 16.04) ... may that be the
>> reason?
>
> I don't
and the latter sources always require extra work to
locate.)
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On 05/02/2019 20:19, Makarius wrote:
> On 05.02.19 11:43, Peter Lammich wrote:
>>
>> Is this worsening due to another Java version, due to the new Isabelle
>> font, or has it some other reasons? How to find out?
>
> From a distance, I would say that this is a matter of
ine. We
are (very slowly) moving towards the Isabelle2019 release (presumably
June 2019), and everything needs to be beyond doubt when released.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On 04/02/2019 14:17, Makarius wrote:
> On 04/02/2019 10:37, Lars Hupel wrote:
>> Is this related to the latest Poly/ML changes? The "slow" job still runs
>> on the x86_64 platform. Last time it worked was 76fbd806ebc5. Hardware
>> is 8-core LRZ VM.
>
On 05.02.19 20:19, Makarius wrote:
From a distance, I would say that this is a matter of the Java 11
font-renderer, which is provided by https://adoptopenjdk.net. The one by
Oracle is much worse -- OpenJdk not the non-free Java. (Note that the
license change of non-free Oracle Java no longer
heap: approx. 350 EUR.
I do see the slight blurring on my ancient HD Sony Vaio from 2013, but I
am not using that very often. Buying a new laptop is certainly more
expensive than just a display -- nonetheless I am surprised how many 100
EUR displays are still standing on desks and stared
to provide the
Generated_Files.add_files facility to 'export_code' -- in parallel to
its existing Export.export. The main difference that this will be an
update on the theory.
(Note that I am presently busy elsewhere and only sporadically connected.)
Makarius
___
is
ces/guide/guide.tex
thys/Sturm_Sequences/guide/isabelle.eps
thys/Sturm_Sequences/guide/isabelle.pdf
description:
proper Isabelle document setup, without generated files in the repository;
It means that the document will also show up in the generated HTML,
similar to the userguide in AFP/Collect
dded support for executable exports in
Isabelle/c175499a7537 -- a few more such fine-tunings might be required.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
(Isabelle/60b5a4731695):
ERROR abort: api.media.atlassian.com certificate error: certificate is
for dentalsaglik.com
There is another benefit for direct browsing: just one uniform HTML view
of repository content, using a current theme provided by Mercurial itself.
Makarius
/devel/build_status/AFP_bulky_64bit_6_threads/index.html
I have switched back to stable polyml-5.7.1-8 for now (see
Isabelle/a5732629cc46) and will be unavailable for the next few days.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailma
On 02/02/2019 15:37, Lawrence Paulson wrote:
> This worked — thanks!
>
>> On 2 Feb 2019, at 13:56, Makarius wrote:
>>
>> Can you try the following in your $ISABELLE_HOME_USER/etc/settings?
>>
>> init_component "$HOME/.isabelle/contrib/polyml-test-1b2dc
On 02/02/2019 14:56, Makarius wrote:
> On 02/02/2019 14:39, Lawrence Paulson wrote:
>> It died twice using “isabelle jedit -l HOL-Analysis”, once using "isabelle
>> jedit Analysis/Analysis.thy” and once using "isabelle build -b HOL-Analysis”.
>>
>> Th
g inherently fragile in concurrent access to a Unix file-system.
These incidents motivated to revive the pending thread to eliminate
physical files from export_code in the first place. Mathematical files
in the theory context are more reliably than physical on
rovements by David Matthews.
After a standard test, I will probably make the above version the
default again.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
FP without problems.
We do continue monotonically towards a stable Poly/ML version: David
Matthews has already sorted out various subtle issues on
https://github.com/polyml/polyml/commits/master -- leading up to current
b68438d33c69.
Makarius
___
is
plemented in
Haskell or OCaml should be particularly easy.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On 31/01/2019 23:11, Makarius wrote:
> *** Isabelle/jEdit Prover IDE ***
>
> * The jEdit File Browser is more prominent in the default GUI layout of
> Isabelle/jEdit: various virtual file-systems provide access to Isabelle
> resources, notably via "favorites:" (or "
y source. Doing this carefully, would even
produce nice PIDE markup for the original sources. PIDE is an IDE for
arbitrary user-defined languages.
It might be worth doing this for tools like Lem eventually, but I have
not looked at it closely so far.
Makarius
___
e of garbage in the natural environment while editing (such as
"export_code ... file ..." with varying file names).
In principle, everything should work on a read-only file-system.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
m to make them fit to
the model. (This sometimes requires minor adjustments of the model.)
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On 31/01/2019 23:11, Makarius wrote:
> *** Isabelle/jEdit Prover IDE ***
>
> * The jEdit File Browser is more prominent in the default GUI layout of
> Isabelle/jEdit: various virtual file-systems provide access to Isabelle
> resources, notably via "favorites:&
entry. Since the latter
is also under PIDE control, CTRL/COMMAND-MOUSE-HOVER-CLICK quickly leads
to some theories.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
s by extra GUI elements. (All other GUI elements
had already options in jEdit or Isabelle).
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On 31/01/2019 20:37, Mathias Fleury wrote:
>
>> On 31. Jan 2019, at 20:10, Makarius >
>> Can you point to these special applications?
>>
>> If export_code uses Generated_Files.add_files (in addition to
>> Export.export) we get both a check for unique
On 31/01/2019 18:27, Peter Lammich wrote:
> On Do, 2019-01-31 at 16:03 +0100, Makarius wrote:
>> I have looked around at typical uses of 'export_code' in AFP. Most of
>> the time it is just informative: writing a file and looking at it in
>> the
>> editor (or via th
e "code/solve.ocaml
in Haskell file "code/"
It could be turned into something like this:
export_code "code/" = solve in OCaml SML Haskell
Some details about the automatic name derivation scheme still need to be
sorted out -- or 'file' remains as an option to specify the suffix for
effective name (without writing anything to the file-system).
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Theory.reset out
of the way in visible Isabelle/ML tool implementations: it is still
present inside Local_Theory.close_target, though.
I wonder what happens when that is removed: presumably it requires a lot
of fine-tuning to make everything work again without that hidden reset.
crash situations that need to be
sorted out.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
er note that --gcthreads is automatically provided, if ML_OPTIONS
does not say anything else.
> 623083120 IsaFoR_2 (1.00)
> 623291272 IsaFoR_2 (1.00)
> 367497971 IsaFoR_2 (0.59)
> 884213127 IsaFoR_2 (1.42) ?
I have briefly tried IsaFoR_
On 23/01/2019 23:44, Makarius wrote:
> Isabelle/20bc1d26c932 now provides an updated polyml-test-a444f281ccec
> (active by default).
>
> It performs slightly better than the previous test version -- I have
> also removed old workarounds for integer arithmetic in
> Isabelle/45912
in
$ISASELLE_HOME_USER/etc/settings are cleaned up, such that this greatest
and latest version gets used.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
nz_C0 (0:06:54 elapsed time, 0:50:34 cpu time, factor 7.33)
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On 23/01/2019 14:14, Bertram Felgenhauer wrote:
> Makarius wrote:
>> On 22/01/2019 12:31, Bertram Felgenhauer wrote:
>>> Makarius wrote:
>>>> So this is the right time for further testing of applications:
>>>> Isabelle2018 should work as well, but I have
On 22/01/2019 23:08, Fabian Immler wrote:
> On 1/22/2019 4:00 PM, Fabian Immler wrote:
>> On 1/22/2019 2:28 PM, Makarius wrote:
>>> On 22/01/2019 20:05, Fabian Immler wrote:
>>>> These numbers look quite extreme:
>>>> The slowdown in polyml-5.
time, somewhere in some
dark corner.
Apart from that, I've recently seen Coq experts worry about the
status-quo of Opam: it is not as well-developed as Stack for Haskell,
and Coq already critically depends on it.
Makarius
___
isabelle-d
o some smaller parts of these sessions, where the effect
is visible? We can then use profiling to get an idea what actually
happens in x86_64_32.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On 19/01/2019 21:43, Makarius wrote:
> Thanks to great work by David Matthews, there is now an Isabelle
> component polyml-test-0a6ebca445fc (Isabelle/3b777286c3ec), which can be
> enabled manually, e.g. in $ISABELLE_HOME_USER/etc/settings like this:
>
> init_component "$HO
On 22/01/2019 12:31, Bertram Felgenhauer wrote:
> Makarius wrote:
>> So this is the right time for further testing of applications:
>> Isabelle2018 should work as well, but I have not done any testing beyond
>> "isabelle build -g main" -- Isabelle development only mo
On 19/01/2019 21:43, Makarius wrote:
> Thanks to great work by David Matthews, there is now an Isabelle
> component polyml-test-0a6ebca445fc (Isabelle/3b777286c3ec), which can be
> enabled manually, e.g. in $ISABELLE_HOME_USER/etc/settings like this:
>
> init_component "$HO
mid-range hardware. There
are additional memory requirements outside the ML heap, for program code
and stacks.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On 18/01/2019 21:55, Tobias Nipkow wrote:
> Hey, I wanted to join the party! But all bugs have been fixed now and
> Makarius will notify you of the correct changeset.
Yes, see Isabelle/b18353d3fe1a.
Despite the carnival season, I am presently working with David Matthews
to make the canon
re is a natural routine of "hg commit" vs. "isabelle build -a" to
make it all work well without any effort.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
ations, including our important
model of having just one branch, i.e. no branches at all. With further
branches, the situation would become much worse, like the average
project on github.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum
On 17/01/2019 21:54, Makarius wrote:
>
> The problem behind this: Angeliki got administrative push-access to the
> Isabelle repository, without anybody at Cambridge showing her how to use it.
>
> There is of course README_REPOSITORY, but the text is long. Here is the
> u
e "hg view" (or equivalent) to ensure that
the change is really what you want to make eternal when pushed to public.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On 14/01/2019 18:47, Makarius wrote:
> The website https://isabelle.in.tum.de appears to be down, this also
> includes the Mercurial repository view at
> https://isabelle.sketis.net/repos/isabelle
>
> Access via SSH works fine, thus the following clone is up-to-date within
> an
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On 11/01/2019 11:51, Makarius wrote:
> On 10/01/2019 16:38, Makarius wrote:
>> On 10/01/2019 16:28, Florian Haftmann wrote:
>>> Code generation: command 'export_code' without file keyword exports
>>> code as regular theory export, which can be materialized using tool
&g
On 10/01/2019 16:38, Makarius wrote:
> On 10/01/2019 16:28, Florian Haftmann wrote:
>> Code generation: command 'export_code' without file keyword exports
>> code as regular theory export, which can be materialized using tool
>> 'isabelle export'; to get generated code du
to write it to the file-system via
Generated_Files.write_files.
* secondary output works via the Export interface to Isabelle/Scala;
e.g. I could easily add Generated_Files.export_files for that and
export_code would merely use Generated_Files.add_files (no
y use double quotes for char/string
literals, instead of slightly odd double single-quotes.
Here is a reminder of the general approach and trend of recent years:
* embedded languages normally use cartouches, while double quotes are
old-style /
ering.
Thus "latest" things require more than one close look before adopting them.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
ng HOL-Library.Cardinal_Notations (which
> HOL-Cardinals.Cardinals does transitively).
It would be great to see this all consolidated and somehow unified, i.e.
some standard notation in Main as proposed by Larry (potentially as
bundles as proposed by Florian), and avoidance of too much no_syntax
rem
On 30/11/2018 21:56, Makarius wrote:
> On 30/11/2018 19:45, Thomas Sewell wrote:
>
> I am also unsure why "archive formats" got on this thread. The heap is a
> binary build artifact, with its own internal structure. Its precise
> content is somewhat non-deterministic,
to refer
persistently to physical file locations, or to build other non-portable
information into the heap.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
tem is more complex and
more easily destroyed by packaging it.
These days I see big and complex products doing it our way: providing a
fully integrated distribution for end-users that by-passes OS package
managers.
Makarius
signature.asc
Description: OpenPGP digital signature
___
On 30/11/2018 16:30, Jonathon Fernyhough wrote:
> On 30/11/2018 14:55, Makarius wrote:
>> On 30/11/2018 14:15, Jonathon Fernyhough wrote:
>>>
>>> I'm currently packaging Isabelle2018 (in deb format) for deployment to
>>> several machines. These packages
On 24/11/2018 19:51, Makarius wrote:
>
> *** Isabelle/jEdit Prover IDE ***
>
> * Fonts for the text area, gutter, GUI elements etc. use the "Isabelle
> DejaVu" collection by default, which provides uniform rendering quality
> with the usual Isabelle symbols.
of it active.
Also note that "isabelle build" uses SHA1 hash keys on the sources, not
datestamps.
Makarius
signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On 24/11/2018 19:51, Makarius wrote:
> *** General ***
>
> * The font family "Isabelle DejaVu" is systematically derived from the
> existing "DejaVu" collection, with variants "Sans Mono", "Sans", "Serif"
> and styles "Norma
v versions might have to revisit their
Isabelle/jEdit properties, to ensure that no "IsabelleText" font
specifications are left. Already existing user properties take
precedence over defaults provided by Isabelle/jEdit: see
$ISABELLE_HOME_USER/jedit/properties vs.
$ISABELLE_HOME/src/Tools/jE
On 15/11/2018 22:13, Makarius wrote:
> On 15/11/2018 19:44, Lawrence Paulson wrote:
>> Got this upon launch. Is it important?
>>
>> 341ebf35464b tip
>>
>> WARNING: Illegal reflective access by macosx.MacOSXPlugin to method
>> com.apple.eawt.Ful
to use fontforge to make a proper font instead.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
uild process
in user-space. It would also mean to get rid of the special "isabelle
jedit -b" in various situations of system initialization.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
hich
where interpreted.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On 08/11/2018 21:32, Makarius wrote:
> Over the decades we have accumulated funny quotation forms in Isabelle
> syntax that are often hard to explain to new users (also to old users).
I don't have a full overview of all the fine points yet, but the general
idea is like this:
* cart
E.g. one could set a date for the "big sweep" and make one big
changeset, or one could gradually update entries in an erratic manner.
You can probably say better if there are problems to be expected between
the "stable" and "d
the document source in the text style of the term
language
At some point there will more Prover IDE support to add/remove the
various formal comments (with control symbols and cartouches) that have
emerged recently. But the old inner syntax is not
On 08/11/2018 21:36, Lawrence Paulson wrote:
>> On 8 Nov 2018, at 20:32, Makarius wrote:
>>
>> In particular, what are the remaining uses of {* ... *}?
>
> I didn’t even know that existed.
It was used a lot with the 'section' and 'text' commands until recently.
Th
ot; to get rid of it (as well as `alt_string`).
The long-term trend is to converge to cartouches or double-quotes almost
everywhere. Cartouches are for nested languages, and double quotes for
string literals or names that are in conflict with other syntax.
tack" and "opam" stack-up considerable material: it
is easy to fill 5-15 GB of disk space after working some time. Only
docker requires even more space.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.in
remove the "isabelle
ghc" tool entry points: these auxiliary scripts should go into
$ISABELLE_HOME/lib/scripts where they cannot be mistaken as regular
Isabelle tools.
I have now also learned that "ghci" is just "ghc --interactive", so
there is no point to treat it too prominently.
On 08/11/2018 12:16, Makarius wrote:
> On 08/11/2018 11:30, Bertram Felgenhauer wrote:
>> Makarius wrote:
>>> Nonetheless, it is still possible to use "isabelle ghc" without stack:
>>> you need to purge the $ISABELLE_STACK_ROOT directory, to prevent the
>&g
On 08/11/2018 11:30, Bertram Felgenhauer wrote:
> Makarius wrote:
>> Nonetheless, it is still possible to use "isabelle ghc" without stack:
>> you need to purge the $ISABELLE_STACK_ROOT directory, to prevent the
>> Isabelle settings mechanism to override ISABELLE_GH
r me, even
with friendly hints via hlint. Unfortunately I failed to reproduce the
installation on my mobile machine. This reminds a bit of ancient times
with vi and emacs, before Isabelle/PIDE/jEdit.
Makarius
___
isabelle-dev mailing list
isabelle-...
On 07/11/2018 16:32, Bertram Felgenhauer wrote:
> Makarius wrote:
>> *** System ***
>>
>> * Support for Glasgow Haskell Compiler via command-line tools "isabelle
>> ghc_setup", "isabelle ghci", "isabelle ghc", "isabelle ghc_st
On 13/10/2018 22:39, Makarius wrote:
>>
>> I've quickly tried openjdk-11 on Ubuntu 18.10 beta: the same low-grade
>> font rendering. It is particularly bad in Isabelle/jEdit file-open dialog.
>
> Thanks to a useful hint by the "Felix von Leitner Institute for
>
, 0:10:40 cpu
> time, factor 1.91)
This is a normal feature of memory management on macOS.
After all these years, David Matthews might eventually want to look if
it is still required these days: for that he merely needs regular SSH
access to some test machine.
Makarius
__
1 - 100 of 2162 matches
Mail list logo
