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
  • 7 years ago
  • 1 hour ago
  • 10 years ago

Installs

  • Total 208
  • Win 112
  • Mac 54
  • Linux 42
Apr 26 Apr 25 Apr 24 Apr 23 Apr 22 Apr 21 Apr 20 Apr 19 Apr 18 Apr 17 Apr 16 Apr 15 Apr 14 Apr 13 Apr 12 Apr 11 Apr 10 Apr 9 Apr 8 Apr 7 Apr 6 Apr 5 Apr 4 Apr 3 Apr 2 Apr 1 Mar 31 Mar 30 Mar 29 Mar 28 Mar 27 Mar 26 Mar 25 Mar 24 Mar 23 Mar 22 Mar 21 Mar 20 Mar 19 Mar 18 Mar 17 Mar 16 Mar 15 Mar 14 Mar 13
Windows 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
Mac 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 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 1 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 | ... ]