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

Details

  • 2017.06.28.18.43.11
  • github.​com
  • github.​com
  • 3 years ago
  • 3 hours ago
  • 6 years ago

Installs

  • Total 160
  • Win 91
  • Mac 32
  • Linux 37
Jun 4 Jun 3 Jun 2 Jun 1 May 31 May 30 May 29 May 28 May 27 May 26 May 25 May 24 May 23 May 22 May 21 May 20 May 19 May 18 May 17 May 16 May 15 May 14 May 13 May 12 May 11 May 10 May 9 May 8 May 7 May 6 May 5 May 4 May 3 May 2 May 1 Apr 30 Apr 29 Apr 28 Apr 27 Apr 26 Apr 25 Apr 24 Apr 23 Apr 22 Apr 21
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 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 1 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 | ... ]