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 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 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
26 matches
Mail list logo
