Re: [isabelle] building the afp sample submission



I am sorry. I think that I did a mistake and downloaded Isabelle 2013
version instead of the latest one.

Viorel


On 05/20/2014 12:00 PM, Fabian Immler wrote:
> You should be able to build the entry [1] (which you can find at [2]) with Isabelle2013-2 (at least I could).
>
> Fabian
>
> [1] http://afp.sourceforge.net/release/afp-Example-Submission-current.tar.gz
> [2] http://afp.sourceforge.net/entries/Example-Submission.shtml
>
> Am 20.05.2014 um 10:50 schrieb Viorel Preoteasa <viorel.preoteasa at aalto.fi>:
>
>> Thank you for your help. I managed to create the basic AFP
>> structure. The Example-Submission is too old and it does
>> not work with isabelle build. I have created my directory
>> based on an ordinary AFP entry. Maybe it would be good
>> if AFP example points to an actual entry in AFP which is
>> always maintained.
>>
>> Best regards,
>>
>> Viorel
>>
>>
>>
>>
>>
>> On 05/19/2014 12:14 PM, Fabian Immler wrote:
>>> Hi,
>>>
>>> Nowadays, sessions are defined in ROOT-files (those can be created with "isabelle mkroot", see Chap. 3 of the Isabelle System Manual).
>>> You build them with "isabelle build", so in the directory containing the submission, you should be able to do:
>>>
>>> "isabelle build -d . Example-Submission"
>>>
>>> or
>>>
>>> "isabelle build -D ."
>>>
>>> Best regards,
>>> Fabian
>>>
>>>
>>> Am 19.05.2014 um 10:57 schrieb Viorel Preoteasa <viorel.preoteasa at aalto.fi>:
>>>
>>>> Hello,
>>>>
>>>> I am trying to build the Isabelle AFP sample submission. I know
>>>> that in the past "isabelle make" did the job, but now make does
>>>> not seem available anymore, and I could not figure out what
>>>> is the replacement.
>>>>
>>>> Best regards,
>>>>
>>>> Viorel Preoteasa
>>>>
>>





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.