Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] building the afp sample submission


view this post on Zulip Email Gateway (Aug 19 2022 at 14:30):

From: Viorel Preoteasa <viorel.preoteasa@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

view this post on Zulip Email Gateway (Aug 19 2022 at 14:30):

From: Fabian Immler <immler@in.tum.de>
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

view this post on Zulip Email Gateway (Aug 19 2022 at 14:31):

From: Viorel Preoteasa <viorel.preoteasa@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

view this post on Zulip Email Gateway (Aug 19 2022 at 14:31):

From: Fabian Immler <immler@in.tum.de>
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

view this post on Zulip Email Gateway (Aug 19 2022 at 14:31):

From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
I am sorry. I think that I did a mistake and downloaded Isabelle 2013
version instead of the latest one.

Viorel


Last updated: Nov 21 2024 at 12:39 UTC