Email Gateway (Aug 19 2022 at 09:00): Email Gateway (Aug 19 2022 at 09:00):From: li yongjian <lyj238@gmail.com>
Hi， Isabelle experts:
I have downloaded the theory package shortest_path from AFP, but
when I run the proof
script dijkstra.thy, it need the Refine_Monadic/Refine.thy, which
in turn need another
theory package collection?
Can anyone tell me how to download all the entries for all the
packages needed?
best
Email Gateway (Aug 19 2022 at 09:00):From: Tobias Nipkow <nipkow@in.tum.de>
The simplest solution is to download the whole AFP - it is not so big (yet).
Here is how you should install and use it: http://afp.sourceforge.net/using.shtml
There is no facility yet to pull in exactly the articles needed.
Best
Tobias
Email Gateway (Aug 19 2022 at 09:01):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Hi,
you can either download the whole AFP as Tobias suggested, or you can use the "Depends On" column in the entry description on
http://afp.sourceforge.net/entries/Dijkstra_Shortest_Path.shtml
In this case it says that you'll need the entries Refine_Monadic and Collections, and Collections needs Binomial-Heaps and Finger-Trees.
I think you have discovered the deepest dependency tree in the whole AFP with this entry -- usually there are 0 or 1 steps only.
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Last updated: Nov 21 2024 at 12:39 UTC