On 30/05/18 11:15, Lars Hupel wrote:
>> The best way maybe is to introduce a dedicated isabelle tool »ocamlc«
>> which uses an environment parameter ISABELLE_OCAML as path prefix to
>> ocamlc / ocamlfind; this would be more pleasant than any kind of ad-hoc
>> montage in ML.
>
> Yes, but we would
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
