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.
>>
>> Or maybe as implicit part of
>>
>> isabelle
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.
>
> Or maybe as implicit part of
>
> isabelle ocaml_setup
Note that any change of the
Or maybe as implicit part of
isabelle ocaml_setup
Sure, that could also work.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
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.
Or maybe as implicit part of
isabelle ocaml_setup
?
Florian
signature.asc
Description: OpenPGP digital signature
isabelle ocaml_opam install zarith
This should ideally happen on-the-fly from within Isabelle/ML.
Cheers
Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
*** System ***
* Update to Poly/ML 5.8 allows to use the native x86_64 platform without
the full overhead of 64-bit values everywhere. This special x86_64_32
mode provides up to 16GB ML heap, while program code and stacks are
allocated elsewhere. Thus approx. 5 times more memory is available for
*** Isabelle/jEdit Prover IDE ***
* Command-line options "-s" and "-u" of "isabelle jedit" override the
default for system option "system_heaps" that determines the heap
storage directory for "isabelle build". Option "-n" is now clearly
separated from option "-s".
*** System ***
* The system
On 05.02.19 13:18, Salomon Sickert wrote:
It should be easy to make this part of the formal session, with some
options [condition = ISABELLE_MLTON].
The 'export_code' command will have to emit generated files
(Generated_Files.add_files) to make the assembly work in Isabelle/ML.
I have
>> To add a couple more to the list:
>>
>> — LTL has includes a parser that is used in an example and built using
>> LTL/examples/build_poly.sh
>>
>> — LTL_to_DRA can generate a tool using either LTL_to_DRA/Code/build_poly.sh
>> and LTL_to_DRA/Code/build_mlton.sh
>
> It should be easy to
On 01/02/2019 15:30, Lars Hupel wrote:
>
> – Sturm_Sequences produces some extra LaTeX documentation. The generated
> PDF is even committed to the AFP.
>
>> * no generated files in the repository (these are not sources but
>> results from sources)
See now
changeset: 10104:394951259923
On 04/02/2019 08:00, Salomon Sickert wrote:
>
>
> To add a couple more to the list:
>
> — LTL has includes a parser that is used in an example and built using
> LTL/examples/build_poly.sh
>
> — LTL_to_DRA can generate a tool using either LTL_to_DRA/Code/build_poly.sh
> and
> On 1. Feb 2019, at 15:30, Lars Hupel wrote:
>
>> What are the remaining uses of these? How much of this can be integrated
>> into the formal Isabelle session? How much of it is actually obsolete?
>
> Hard to tell from a distance, but here's what I gather from reading the
> Makefiles:
>
> –
On 02/02/2019 14:13, Florian Haftmann wrote:
> * The module naming schema gets more sophisticated: default, name or
> prefix. The key point is that this naming schema is again
> target-language specific.
Just abstractly, a reform should strive for unification and
simplification whenever
>> Maybe the »checking« should just be a variant of the regular export.
>>
>> Hence the modification could be quite conservative:
>>
>> export_code CONSTS in LANGUAGE ( '(' OPTIONS ')' ) ( module_name NAME )
>> ( file … | ( prefix … ) ( checked ) )
>>
>> where »file« denotes a relative root
On 01/02/2019 16:40, Lars Hupel wrote:
>> The standard approach for the latter is to have the other tool directly
>> import its source format into the theory context within Isabelle/ML,
>> without the intermediate theory source. Doing this carefully, would even
>> produce nice PIDE markup for the
> The standard approach for the latter is to have the other tool directly
> import its source format into the theory context within Isabelle/ML,
> without the intermediate theory source. Doing this carefully, would even
> produce nice PIDE markup for the original sources. PIDE is an IDE for
>
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 "Edit Favorites").
I have now
On 01/02/2019 15:30, Lars Hupel wrote:
>
>> * no generated files in the repository (these are not sources but
>> results from sources)
>
> What about generated theory files? This also affects the CakeML entry. I
> could easily package Lem as a component, but how would "isabelle build"
> call
> What are the remaining uses of these? How much of this can be integrated
> into the formal Isabelle session? How much of it is actually obsolete?
Hard to tell from a distance, but here's what I gather from reading the
Makefiles:
– Formal_SSA appears to download some file, unpack it, and
On 01/02/2019 14:29, Lars Hupel wrote:
>> In 2012 we eliminated all Makefiles from AFP: I did not know that some
>> came back, or chose to ignore it.
>
> ~/work/afp (default)$ find thys/ -name Makefile
> thys/Buchi_Complementation/code/Makefile
> thys/Formal_SSA/Makefile
>
> In 2012 we eliminated all Makefiles from AFP: I did not know that some
> came back, or chose to ignore it.
~/work/afp (default)$ find thys/ -name Makefile
thys/Buchi_Complementation/code/Makefile
thys/Formal_SSA/Makefile
thys/LightweightJava/ott-src/Makefile
thys/Sturm_Sequences/guide/Makefile
On 01/02/2019 12:43, Lars Hupel wrote:
>
> It would like to reiterate that the technical part of this issue is the
> easy bit. The difficult bit is deciding policy: Should Isabelle
> committers be responsible for breakage in downstream artifacts? In other
> words, should the AFP stability
> 1. Gratchk is a similar use-case, where I need to export code, link it
> with some external ML code using MLton b/c it's faster, and test the
> result for timing regressions. Because gratchk is also bundled with
> gratgen, which is implemented in C++, I have not yet put it into the
> AFP, b/c
Can you give some more details on how to achieve this?
>
> Concrete application: I have a verified SAT solver (lets call that
1. Gratchk is a similar use-case, where I need to export code, link it
with some external ML code using MLton b/c it's faster, and test the
result for timing
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 "Edit Favorites").
There is an
*** 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 "Edit Favorites").
* Action "isabelle-export-browser" points the File Browser
*** Isabelle/jEdit Prover IDE ***
* System option "jedit_text_overview" allows to disable the text
overview column.
This refers to Isabelle/5a8ae7a4b7d0 -- it is a minor visual enhancement
for situations where the editor screen should look like a presentation,
without any distractions by extra
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 names and an easy way to
>> retrieve the
Hi Makarius,
> On 31. Jan 2019, at 20:10, Makarius wrote:
>
> 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
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 the command-line!?), or doing that
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 the command-line!?), or doing that on the output
> channel.
> The isabelle-export:
On 14/01/2019 20:20, Florian Haftmann wrote:
>
>> * Are there remaining uses of 'file' with empty name? Is the virtual
>> file-system browser sufficiently convenient to inspect results
>> interactively?
>
> I checked the file system browser and would be quite content with it; as
> a bonus you
Hi Makarius,
> * Are there remaining uses of 'file' with empty name? Is the virtual
> file-system browser sufficiently convenient to inspect results
> interactively?
I checked the file system browser and would be quite content with it; as
a bonus you can then make use of the syntax
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
>>> 'isabelle export'; to get
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 dumped into output, use
>>
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 dumped into output, use
> 'file ""'. Minor INCOMPATIBILITY.
>
> This
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 dumped into output, use
'file ""'. Minor INCOMPATIBILITY.
This refers to e02bdf853a4c and opens opportunities to get
*** System ***
* The command-line tool "isabelle update" uses Isabelle/PIDE in
batch-mode to update theory sources based on semantic markup produced in
Isabelle/ML. Actual updates depend on system options that may be enabled
via "-u OPT" (for "update_OPT"), see also $ISABELLE_HOME/etc/options
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. For Java/Swing GUI elements this
>
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 "Normal", "Bold", "Italic/Oblique", "Bold-Italic/Oblique".
> The DejaVu base
*** General ***
* The font family "Isabelle DejaVu" is systematically derived from the
existing "DejaVu" collection, with variants "Sans Mono", "Sans", "Serif"
and styles "Normal", "Bold", "Italic/Oblique", "Bold-Italic/Oblique".
The DejaVu base fonts are retricted to well-defined Unicode ranges
On 11/11/2018 16:44, Lars Hupel wrote:
>> * Support for Isabelle command-line tools defined in Isabelle/Scala.
>> Instances of class Isabelle_Scala_Tools may be configured via the shell
>> function "isabelle_scala_tools" in etc/settings (e.g. of an Isabelle
>> component).
>
> This is nice!
* Support for Isabelle command-line tools defined in Isabelle/Scala.
Instances of class Isabelle_Scala_Tools may be configured via the shell
function "isabelle_scala_tools" in etc/settings (e.g. of an Isabelle
component).
This is nice! Anything on the radar to automate compilation as well,
*** System ***
* Support for Isabelle command-line tools defined in Isabelle/Scala.
Instances of class Isabelle_Scala_Tools may be configured via the shell
function "isabelle_scala_tools" in etc/settings (e.g. of an Isabelle
component).
This refers to Isabelle/258bef08b31e. In recent years we
This is the updated situation according to Isabelle/c1a27fce2076:
*** System ***
* Support for managed installations of Glasgow Haskell Compiler and
OCaml via the following command-line tools:
isabelle ghc_setup
isabelle ghc_stack
isabelle ocaml_setup
isabelle ocaml_opam
The global
Makarius wrote:
> On 08/11/2018 14:59, Bertram Felgenhauer wrote:
> >>
> >> I've misunderstood the problem. You intend to invoke old-style
> >> $ISABELLE_GHC via the new-style "isabelle ghc" interface, but within
> >> Isabelle/ML sessions the standard way is still $ISABELLE_GHC in both cases.
> >
On 08/11/2018 14:59, Bertram Felgenhauer wrote:
>>
>> I've misunderstood the problem. You intend to invoke old-style
>> $ISABELLE_GHC via the new-style "isabelle ghc" interface, but within
>> Isabelle/ML sessions the standard way is still $ISABELLE_GHC in both cases.
>
> This may be premature,
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
> >> Isabelle settings mechanism to override ISABELLE_GHC with
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
>>> Isabelle settings mechanism to override
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_GHC with the
>> stack-based tools.
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_GHC with the
> stack-based tools.
After purging $ISABELLE_STACK_ROOT, `isabelle ghc`
*** System ***
* Session directory $ISABELLE_HOME/src/Tools/Haskell provides some
source modules for Isabelle tools implemented in Haskell, notably for
Isabelle/PIDE.
This refers e.g. to current Isabelle/438e1a11445f.
There is more and more material emerging: as direct ports from
Isabelle/ML
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_stack".
>> Existing settings variable ISABELLE_GHC is maintained
Makarius wrote:
> *** System ***
>
> * Support for Glasgow Haskell Compiler via command-line tools "isabelle
> ghc_setup", "isabelle ghci", "isabelle ghc", "isabelle ghc_stack".
> Existing settings variable ISABELLE_GHC is maintained dynamically
> according the state of ISABELLE_STACK_ROOT and
On 22/10/2018 14:05, Lars Hupel wrote:
The binary provided by Homebrew does not exhibit that problem. I have no
other information beyond that.
I'm trying out a High Sierra Mac Book Pro, and Stack appears to work there.
Interestingly enough, I get Poly/ML warnings of the form:
14:11:19
On 22/10/2018 15:05, Lars Hupel wrote:
>
> I'm trying out a High Sierra Mac Book Pro, and Stack appears to work there.
>
> Interestingly enough, I get Poly/ML warnings of the form:
>
> 14:11:19 poly(50366,0xb042) malloc: *** mach_vm_map(size=8388608)
> failed (error code=3)
> 14:11:19 ***
> The binary provided by Homebrew does not exhibit that problem. I have no
> other information beyond that.
I'm trying out a High Sierra Mac Book Pro, and Stack appears to work there.
Interestingly enough, I get Poly/ML warnings of the form:
14:11:19 poly(50366,0xb042) malloc: ***
> Can you actually explain the problem and its solution?
The problem appears to be that the official Stack binaries do not work
consistently on El Capitan. The machine I've tried them on is fully
updated and has no special software setup.
The binary provided by Homebrew does not exhibit that
On 21/10/2018 17:34, Lars Hupel wrote:
>> On an El Capitan system, this produces the following error:
>
> The problem can alternatively be solved by installing Homebrew's stack
> version and declaring
>
> ISABELLE_STACK="/usr/local/bin/stack"
>
> in ~/.isabelle/etc/settings.
Can you actually
> On an El Capitan system, this produces the following error:
The problem can alternatively be solved by installing Homebrew's stack
version and declaring
ISABELLE_STACK="/usr/local/bin/stack"
in ~/.isabelle/etc/settings.
___
isabelle-dev mailing list
> * Support for Glasgow Haskell Compiler via command-line tools "isabelle
> ghc_setup", "isabelle ghci", "isabelle ghc", "isabelle ghc_stack".
> Existing settings variable ISABELLE_GHC is maintained dynamically
> according the state of ISABELLE_STACK_ROOT and ISABELLE_STACK_RESOLVER.
Just a side
On 21/10/2018 13:25, Lars Hupel wrote:
>> * Support for Glasgow Haskell Compiler via command-line tools "isabelle
>> ghc_setup", "isabelle ghci", "isabelle ghc", "isabelle ghc_stack".
>> Existing settings variable ISABELLE_GHC is maintained dynamically
>> according the state of ISABELLE_STACK_ROOT
> * Support for Glasgow Haskell Compiler via command-line tools "isabelle
> ghc_setup", "isabelle ghci", "isabelle ghc", "isabelle ghc_stack".
> Existing settings variable ISABELLE_GHC is maintained dynamically
> according the state of ISABELLE_STACK_ROOT and ISABELLE_STACK_RESOLVER.
On an El
*** System ***
* Support for Glasgow Haskell Compiler via command-line tools "isabelle
ghc_setup", "isabelle ghci", "isabelle ghc", "isabelle ghc_stack".
Existing settings variable ISABELLE_GHC is maintained dynamically
according the state of ISABELLE_STACK_ROOT and ISABELLE_STACK_RESOLVER.
> * How to re-init the opam installation, e.g. after changing
> ISABELLE_OCAML_VERSION (maybe even in ISABELLE_HOME_USER/etc/settings)?
> (Presently I have just removed purged ISABELLE_OPAM_ROOT.)
I don't think purging the directory is necessary. It should work out of
the box. According to
This refers to AFP/c245a746483a and Isabelle/337b8ce5ff8d.
The CakeML compiler is now available from within Isabelle/ML.
Steps to use:
1) echo 'init_components "$HOME/.isabelle/contrib"
"$ISABELLE_HOME/Admin/components/cakeml"' >> ~/.isabelle/etc/settings
2) echo 'ISABELLE_CC=gcc' >>
On 24/09/18 08:19, Lars Hupel wrote:
>> There were a few remaining uses in AFP. Notable changes are
>> AFP/58b893c52562 and AFP/bf2659bf0a46, where I had to edit sources
>> generated by LEM (!). I don't know how LEM is maintained: it needs to
>> produce different inner comments next time, and can
> There were a few remaining uses in AFP. Notable changes are
> AFP/58b893c52562 and AFP/bf2659bf0a46, where I had to edit sources
> generated by LEM (!). I don't know how LEM is maintained: it needs to
> produce different inner comments next time, and can actually use
> \ CARTOUCHE notation
*** General ***
* Old-style inner comments (* ... *) within the term language are no
longer supported (legacy feature in Isabelle2018).
This refers to Isabelle/6e9df530b441.
There were a few remaining uses in AFP. Notable changes are
AFP/58b893c52562 and AFP/bf2659bf0a46, where I had to edit
*** Isar ***
* Implicit cases goal1, goal2, goal3, etc. have been discontinued
(legacy feature since Isabelle2016).
This refers to 8c240fdeffcb. The NEWS for Isabelle2016 already explain
that the proof method "goal_cases" is the proper way to do it.
Makarius
*** ML ***
* Original PolyML.pointerEq is retained as a convenience for tools that
don't use Isabelle/ML (where this is called "pointer_eq").
* ML evaluation (notably via commands 'ML' and 'ML_file') is subject to
option ML_environment to select a named environment, such as "Isabelle"
for
*** Document preparation ***
* System option "document_tags" specifies alternative command tags. This
is occasionally useful to control the global visibility of commands via
session options (e.g. in ROOT).
This refers to Isabelle/88b0e63d58a5, which also provides the updated
documentation. The
I just tried
isabelle jedit -R HOL-UNITY
assuming that it would build an auxiliary image for HOL-Auth, which is
imported. It built HOL-Auth rather than HOL-UNITY_requirements(HOL-Auth) so
things are pretty subtle here. A little more explanation would be valuable.
Larry
> On 6 Jun
On 06/06/18 16:19, Lawrence Paulson wrote:
>
> According to the NEWS entry, option -R builds an auxiliary logic image. I
> tried this with a couple of examples and no images were built. According to
> the manual, this option opens the ROOT entry. It does seem to do that, though
> I'm not sure
> On 6 Jun 2018, at 12:43, Makarius wrote:
>
> On 06/06/18 12:45, Lawrence Paulson wrote:
>> I saw them of course, but what do they do?
>
> These options go back to Nov-2017, but in recent Isabelle/bcdc47c9d4af I
> have simplified and clarified the situation, updated NEWS and
> documentation in
On 06/06/18 12:45, Lawrence Paulson wrote:
> I saw them of course, but what do they do?
These options go back to Nov-2017, but in recent Isabelle/bcdc47c9d4af I
have simplified and clarified the situation, updated NEWS and
documentation in the "jedit" manual.
Right now the main question is if
> Am 05.06.2018 um 23:01 schrieb Makarius :
>
> These options are very relevant for the coming release. I am interested
> to get feedback from early adopters, if this is already sufficient or
> requires further refinement.
>
> In other words, the question behind this: Can be get rid of most
>
I saw them of course, but what do they do?
Larry
> On 5 Jun 2018, at 22:19, Makarius wrote:
>
> On 05/06/18 23:06, Lawrence Paulson wrote:
>> I’d find an example helpful, as your brief description is pretty cryptic.
>> Larry
>>
>>> On 5 Jun 2018, at 22:01, Makarius wrote:
>>>
>>> These
On 05/06/18 23:06, Lawrence Paulson wrote:
> I’d find an example helpful, as your brief description is pretty cryptic.
> Larry
>
>> On 5 Jun 2018, at 22:01, Makarius wrote:
>>
>> These options are very relevant for the coming release. I am interested
>> to get feedback from early adopters, if
I’d find an example helpful, as your brief description is pretty cryptic.
Larry
> On 5 Jun 2018, at 22:01, Makarius wrote:
>
> These options are very relevant for the coming release. I am interested
> to get feedback from early adopters, if this is already sufficient or
> requires further
On 04/06/18 14:27, Makarius wrote:
> *** Isabelle/jEdit Prover IDE ***
>
> * The command-line tool "isabelle jedit" provides more flexible options
> for session management:
> - option -R builds an auxiliary logic image with all required theories
> from other sessions, relative to an
On 05/06/18 14:54, Fabian Immler wrote:
>
>> What kind of theory is this? Many commands? Long-running /
>> non-terminating commands?
> In this particular case, it was a relatively short theory (300 lines) with no
> long-running or non-terminating commands. I inserted and removed some
>
> Am 05.06.2018 um 14:47 schrieb Makarius :
>
> On 05/06/18 14:45, Fabian Immler wrote:
>>
>>
The only way to stop this apparently is to invalidate something in the
beginning of the (currently open) theory.
>>>
>>> It should be possible to achieve this effect by removing the
On 05/06/18 14:45, Fabian Immler wrote:
>
>
>>> The only way to stop this apparently is to invalidate something in the
>>> beginning of the (currently open) theory.
>>
>> It should be possible to achieve this effect by removing the concluding
>> 'end' command.
> Just now I was in the middle of a
> Am 05.06.2018 um 13:39 schrieb Makarius :
>
> On 04/06/18 20:17, Fabian Immler wrote:
>>
>> This "something in the background" appears to happen on a regular basis:
>> every 2-3 seconds, the poly process consumes 200%CPU for about a second.
>> poly should be idle (or used to be in such a
On 04/06/18 20:17, Fabian Immler wrote:
>
> This "something in the background" appears to happen on a regular basis:
> every 2-3 seconds, the poly process consumes 200%CPU for about a second.
> poly should be idle (or used to be in such a situation) because (as far
> as I can tell) nothing else
*** Isabelle/jEdit Prover IDE ***
* The command-line tool "isabelle jedit" provides more flexible options
for session management:
- option -R builds an auxiliary logic image with all required theories
from other sessions, relative to an ancestor session given by option
-A (default:
*** Isabelle/jEdit Prover IDE ***
* Slightly more parallel checking, notably for high priority print
functions (e.g. State output).
This refers to Isabelle/b00b40dc41af -- with various fine points in the
organization of PIDE execution forks, not just the preceeding cd387c55e085.
As we are
*** System ***
* The command-line tool "dump" dumps information from the cumulative
PIDE session database: many sessions may be loaded into a given logic
image, results from all loaded theories are written to the output
directory.
This refers to Isabelle/2ac3a5c07dfa. It is a spin-off from
*** ML ***
* Command 'ML_export' exports ML toplevel bindings to the global
bootstrap environment of the ML process. This allows ML evaluation
without a formal theory context, e.g. in command-line tools like
"isabelle process".
This refers to Isabelle/cbee43ff4ceb.
Here are also the examples
Just for the record: Makarius' reply resolved the issue for me (see also
below).
On 05/09/2018 11:57 PM, Makarius wrote:
> On 26/03/18 13:48, Christian Sternagel wrote:
>>
>> Thanks, I forgot about that option.
>>
>> With "isabelle latex" in the specified directory the error boils down to:
>>
>>
On 26/03/18 13:48, Christian Sternagel wrote:
>
> Thanks, I forgot about that option.
>
> With "isabelle latex" in the specified directory the error boils down to:
>
> ./root.tex:31: Package pdftex.def Error: File
> `isabelle-eps-converted-to.pdf' n
> ot found.
>
> See the pdftex.def package
*** Isabelle/jEdit Prover IDE ***
* Update to jedit-5.5.0, the latest release.
This refers to Isabelle/752a4e6d760c. Relatively little has happened,
but there are some preparations for Java 9. We are still on Java 8, even
though Java 10 has been released recently. I will soon make some
Dear Makarius,
Thanks, I forgot about that option.
With "isabelle latex" in the specified directory the error boils down to:
./root.tex:31: Package pdftex.def Error: File
`isabelle-eps-converted-to.pdf' n
ot found.
See the pdftex.def package documentation for explanation.
Type H for
On 26/03/18 09:33, Christian Sternagel wrote:
>
> I don't see a significant difference in output between my original
>
> isabelle build_doc system
> *** Failed to build document in
> "/tmp/isabelle-griff/document_output1585848392449927242/system"
>
> and the suggested
>
> isabelle build
Dear Makarius,
I don't see a significant difference in output between my original
isabelle build_doc system
where I get
...
isabelle document -d
/tmp/isabelle-griff/document_output1585848392449927242/system -o pdf -n
system
*** Failed to build document in
On 23/03/18 10:29, Christian Sternagel wrote:
>
> Is there a way to get a more detailed report on why the last step,
> "isabelle document ...", failed?
>
> Btw: I also get (sometimes more specific) errors for building other
> documentation.
>
> Okay, turns out that I was missing the LaTeX
Dear Makarius,
I am on 67927:0b70405b3969 and
./bin/isabelle build_doc system
doesn't work for me. I get the error:
Build started for documentation "system"
Cleaning System ...
Running System ...
System FAILED
...
isabelle document -d
On 19/03/18 19:35, Makarius wrote:
> *** System ***
>
> * The command-line tools "isabelle server" and "isabelle client" provide
> access to the Isabelle Server: it supports responsive session management
> and concurrent use of theories, based on Isabelle/PIDE infrastructure.
> See also the
*** System ***
* The command-line tools "isabelle server" and "isabelle client" provide
access to the Isabelle Server: it supports responsive session management
and concurrent use of theories, based on Isabelle/PIDE infrastructure.
See also the "system" manual.
This refers to
1 - 100 of 766 matches
Mail list logo
