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
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
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
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
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