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 language syntax, clafer, compiler, instance generator

Details

  • 2017.06.28.18.43.11
  • github.​com
  • github.​com
  • 8 years ago
  • 43 minutes ago
  • 11 years ago

Installs

  • Total 232
  • Win 126
  • Mac 62
  • Linux 44
Oct 26 Oct 25 Oct 24 Oct 23 Oct 22 Oct 21 Oct 20 Oct 19 Oct 18 Oct 17 Oct 16 Oct 15 Oct 14 Oct 13 Oct 12 Oct 11 Oct 10 Oct 9 Oct 8 Oct 7 Oct 6 Oct 5 Oct 4 Oct 3 Oct 2 Oct 1 Sep 30 Sep 29 Sep 28 Sep 27 Sep 26 Sep 25 Sep 24 Sep 23 Sep 22 Sep 21 Sep 20 Sep 19 Sep 18 Sep 17 Sep 16 Sep 15 Sep 14 Sep 13 Sep 12 Sep 11
Windows 0 0 0 0 1 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1
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 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 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

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 | ... ]