Isabelle tips and tricks

Using Isabelle as an external prover for Why3

In order to use Isabelle as an external prover for Why3, you need to install Isabelle2014 (for Why3 0.86.2).

To allow why3 config --detect-provers to find this version of Isabelle, you can put the following script in /usr/local/bin/isabelle (do not forget chmod +x /usr/local/bin/isabelle):

#!/bin/sh
dir=/Applications/Isabelle2014.app/Contents/Resources/Isabelle2014
env ISABELLE_HOME=$dir $dir/bin/isabelle $*

Replace the value of dir with the Isabelle home of your installation. The example above is OK on a Mac.

Some files are missing in the lib/why3/isabelle directory of the Why3 distribution. You can get them here.

You have to add the following line to the etc/components file of your Isabelle2014 installation:

/Users/<user name>/.opam/system/lib/why3/isabelle

replacing <user name> with your user name. If you did not install Why3 with opam, replace this with the equivalent path in your installation of Why3.

Making the Finder open a .thy file in Isabelle

On Mac OS, Isabelle is packaged as an application, but some information is missing about it to make the Finder open theory files in Isabelle when you double-click them. To fix this, just add the following entry in the Info.plist file which is located in the Contents directory inside the bundle of the application:

<key>CFBundleDocumentTypes</key>
<array>
  <dict>
    <key>CFBundleTypeExtensions</key>
    <array>
      <string>thy</string>
    </array>
    <key>CFBundleTypeIconFile</key>
    <string>theory.icns</string>
    <key>CFBundleTypeOSTypes</key>
    <array>
      <string>****</string>
      <string>fold</string>
    </array>
    <key>CFBundleTypeRole</key>
    <string>Viewer</string>
  </dict>
</array>

After the modification, the head of the Info.plist file should look like:

<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE plist PUBLIC "-//Apple//DTD PLIST 1.0//EN" "http://www.apple.com/DTDs/PropertyList-1.0.dtd">
<plist version="1.0">
<dict>
<key>CFBundleDocumentTypes</key>
<array>
  <dict>
    <key>CFBundleTypeExtensions</key>