Re: [isabelle-dev] NEWS: generated code as proper theory export

2019-02-05 Thread Salomon Sickert

>> 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 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 already added support for executable exports in
> Isabelle/c175499a7537 -- a few more such fine-tunings might be required.

That is a great development. 

Could someone point me to an example on how to do compilation with either mlton 
or polyml within a formal session?
The build scripts in these two entries are copying the style of the CAVA entry 
at that time and I’m not sure about the current best practices here.

Best,
Salomon
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] NEWS: generated code as proper theory export

2019-02-03 Thread Salomon Sickert

> 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:
> 
> – Formal_SSA appears to download some file, unpack it, and compile
> generated code together with it.
> 
> – Lightweight_Java generates an Isabelle theory file with Ott.
> 
> – Buchi_Complementation compiles generated code with MLton.
> 
> – Sturm_Sequences produces some extra LaTeX documentation. The generated
> PDF is even committed to the AFP.

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

Best,
Salomon

>>  * 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 it?
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] PLATFORMS: Mac OS X

2017-04-07 Thread Salomon Sickert

>> In this case I recommend to bump the baseline for Ubuntu up to 14.04 LTS
>> (or even 16.04 LTS).
> 
> How did you get to that conclusion? Ubuntu LTS support lasts 5 years.
> Empiricially, I've seen the last 3 LTS versions being installed by
> Isabelle users. Consequently, we have only recently dropped 10.04 LTS
> and are now at 12.04 LTS for some years to come.

The current date is 7.4.2017. Thus this is the last month of support for 12.04 
LTS. 

>> And secondly dropping support for OS X Mavericks, since that is also
>> unsupported by Apple right now.
> 
> Dropping Mavericks now would mean to reinstall macbroy2, which is our
> main witness for non-trivial Apple hardware. Such a change comes with
> the risk that the system stops working afterwards: the old saying "never
> change a running system" has some truth in it.

I don’t get why supporting fewer systems is more work. But anyways it was just 
a suggestion.

Best,
Salomon

smime.p7s
Description: S/MIME cryptographic signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] PLATFORMS: Mac OS X

2017-04-05 Thread Salomon Sickert
Hi Makarius,

> Please regard the updated Admin/PLATFORMS file
> http://isabelle.in.tum.de/repos/isabelle/annotate/27c1b5e952bd/Admin/PLATFORMS
>  
> 

Looking through the list of supported platforms I was wondering, how the 
deprecation cycle works.
Wouldn’t it be a good idea to drop support for a platform if the vendor stops 
supporting it?

In this case I recommend to bump the baseline for Ubuntu up to 14.04 LTS (or 
even 16.04 LTS).
And secondly dropping support for OS X Mavericks, since that is also 
unsupported by Apple right now.

What do you think?

Best,
Salomon

smime.p7s
Description: S/MIME cryptographic signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] Isabelle/jEdit - Loading of AFP session images fails

2016-03-30 Thread Salomon Sickert

> When there is a problem there are two possibilities:
> 
> (1) Someone who understands the relevant part of the system knows what needs 
> to be done. This is the case here, see now c35012b86e6f.

Thank you. It works now as expected.

> (2) If nobody has concrete ideas, Mercurial allows to make empiric studies of 
> the history via bisection.
> 
> The history is the "proof" for the state of the sources. This is why it is 
> important to keep the history clean and easy to understand -- after months, 
> years, decades.

Let me rephrase my question: I wanted to know, if there is a way to get 
something more helpful from Isabelle/jEdit, like a stack trace or a debug log. 

Best,
Salomon
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


[isabelle-dev] Isabelle/jEdit - Loading of AFP session images fails

2016-03-29 Thread Salomon Sickert
Hello all,

I’m currently working with the current isabelle-devel (fe827c6fa8c5) and 
afp-devel (6143a36 
)
 and I have issues loading session images built from the AFP. For example 
loading HOL-Library works fine:

> sickert$ bin/isabelle jedit -d "~/Documents/workspace/afp-devel/thys/" -l 
> HOL-Library

However, if I want to load a session from the AFP:

> sickert$ bin/isabelle jedit -d "~/Documents/workspace/afp-devel/thys/" -l 
> Automatic_Refinement
1:32:14 PM [Session.manager] [error] manager: *** Consumer thread failure: 
"Session.manager"
1:32:14 PM [Session.manager] [error] manager: *** Undefined session: 
“Automatic_Refinement"

The puzzling thing is, that Isabelle finds the session “Automatic_Refinement”, 
builds it and then complains that it doesn’t know what is. 
Any ideas on how to debug and fix this?

Thank you,
Salomon___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev