ctrl+shift+p filters: :st2 :st3 :win :osx :linux
Browse

Clafer Tools

by gsdlab ALL

Integration of Clafer Compiler and Instance Generators into Sublime Text 2/3

Labels Clafer, Compiler, Instance Generator

Details

  • 2017.06.28.18.43.11
  • github.​com
  • github.​com
  • 8 years ago
  • 1 hour ago
  • 10 years ago

Installs

  • Total 220
  • Win 117
  • Mac 60
  • Linux 43
Jan 3 Jan 2 Jan 1 Dec 31 Dec 30 Dec 29 Dec 28 Dec 27 Dec 26 Dec 25 Dec 24 Dec 23 Dec 22 Dec 21 Dec 20 Dec 19 Dec 18 Dec 17 Dec 16 Dec 15 Dec 14 Dec 13 Dec 12 Dec 11 Dec 10 Dec 9 Dec 8 Dec 7 Dec 6 Dec 5 Dec 4 Dec 3 Dec 2 Dec 1 Nov 30 Nov 29 Nov 28 Nov 27 Nov 26 Nov 25 Nov 24 Nov 23 Nov 22 Nov 21 Nov 20
Windows 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 1 0
Mac 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
Linux 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0

Readme

Source
raw.​githubusercontent.​com

Clafer Tools

v0.4.5

Integration of Clafer Compiler and Instance Generators into Sublime Text 2/3.

See release notes for Clafer 0.4.5.

Contributors

Features and Usage

  • Syntax highlighting of keywords, operators, comments, and integer and string literals
  • Compilation and validation <CTRL>+b. To change parameters of the command:
    • Preferences->Browse Packages
    • cd Clafer Tools
    • edit Clafer.sublime-build
  • Instance generation (with simple scope inference) using
    • Alloy-based instance generator <CTRL>+i, g, a
    • Choco-based instance generator <CTRL>+i, g, c
    • Z3 SMT-based instance generator <CTRL>+i, g, s (only for 0.3.6.1)

Installation

  1. Install Sublime Text 3. On Ubuntu, add the WebUpd8 PPA then execute sudo apt install sublime-text-installer.
  2. In Sublime Text
    • Install Package Control
      • Tools->Install Package Control...
    • Install packages SublimeREPL, Clafer Tools and (optionally) SidebarEnhancements
      • Preferences->Package Control->Install Package
      • type the name of the package
    • Open the Packages folder
      • Preferences->Browse Packages...
      • copy the folder SublimeREPL from Clafer Tools to Packages
        • on Mac, use the merge option not replace
  3. Download the latest binary distribution of Clafer Tools
    • Clafer Tools
    • Unzip the contents of the folder clafer-tools-0.4.5 into Packages/Clafer-Bin
      • Make sure the folder structure is NOT Packages/Clafer-Bin/clafer-tools-0.4.5, that is, the contents of the folder clafer-tools-0.4.5 are directly inside Clafer-Bin
    • (optional) add Clafer-Bin to the variable PATH.
  4. On Windows only
    • Alloy-based instance generator only works with 32bit Java on Windows and if you only have 64bit Java installation, you will see an error: Exception in thread "main" java.lang.UnsatisfiedLinkError: no minisatproverx1 in java.library.path.

Known Limitations and Workarounds

  • On Windows - Setting the PATH to 32bit Java installation

    • install 32bit JDK but do not modify the PATH to point to it (there's no 32bit JRE anymore)
    • in Sublime Text
      • Preferences->Package Settings->SublimeREPL->Settings - Default
      • set default_extended_env as "default_extend_env": {"PATH": "C:/Program Files (x86)/Java/jdk1.8.0_102/bin;{PATH}"},

  • On Linux and Mac

    • the Python 3 executable is called python3 and the best solution is to create a symlink called python pointing to /usr/bin/python3
      • in Packages/Clafer Tools execute ln -s /usr/bin/python3 python.
    • it's also needed to add the current directory . to the PATH, so that the executables are found. Add the following line at the end of your .profile
      • PATH=".:$PATH"
    • for python to be able to find the Z3 library, add the following line to your .profile
      • on Linux, export LD_LIBRARY_PATH="~/.config/sublime-text-3/Packages/Clafer-Bin:$LD_LIBRARY_PATH"
      • on Mac, export DYLD_LIBRARY_PATH="~/.config/sublime-text-3/Packages/Clafer-Bin:$DYLD_LIBRARY_PATH"

  • On MacOS Yosemite, the preferred way of setting the variable PATH is by editing /etc/paths. However, despite that, Sublime Text 2/3 will not see the specified values because it is a GUI application and it will only see /usr/bin:/bin:/usr/sbin:/sbin:/. To check the value of PATH visible to Sublime

    1. open console View->Show Console
    2. execute import os; print (os.environ['PATH'])
    3. if you see /usr/bin:/bin:/usr/sbin:/sbin:/, you are affected by the Yosemite PATH bug and ClaferChocoIG will be unable to comple the model for you because it calls the clafer executable.
    4. the workaround is to:
      • create a symlink sudo ln -s ~/Library/Application\ Support/Sublime\ Text\ 3/Packages/Clafer-Bin/clafer /usr/bin/clafer so that clafer executable will be visible on the default PATH.
    5. to conveniently use ClaferChocoIG, move the script claferchocoig.sh (included in Mac binary distro) to /usr/bin by executing sudo mv ~/Library/Application\ Support/Sublime\ Text\ 3/Packages/Clafer-Bin/claferchocoig.sh /usr/bin.

  • ClaferSMT in Clafer Tools 0.3.6.1 binary depends on the python package bintrees, to install execute pip install bintrees on Windows or pip3 install bintrees on Linux and Mac.

Planned Improvements

  • Code snippets for quantified expressions such as [ all disj x1; x2 : X | ... ]