LoginSignup
1
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

More than 3 years have passed since last update.

@electronics_diy721(elec tron)

MacBookにliquidhaskellをインストール

Last updated at Posted at 2021-10-22

データ型が持つことが許される値の範囲を定義したり（依存型 dependent type）、型が持つことを許される値を関数で定義（篩型 refinement type）した上で、Haskellで定義された型制約が守られているかをコンパイル時に型検査できる__liquidhaskell__をインストールしたい。

依存型と篩型は、Idris, Racket（LISP方言のSchemeのそのまた方言・・・自己再帰・・・）, Standard ML（SML）, F*（F#ではない）, Scala, TypeScriptと、関数型言語を中心に、Java派生（Scala）やJavaScript派生のAltJS（TypeScript）言語でも、徐々に取り入れられつつある型定義の機能です。

__git cloneとstack install__の組み合わせで、MacBookにliquidhaskellをインストールすることができました。以下の２つは、失敗しました。

  • cabal install liquidhaskell
  • cabal install liquid-platform

この記事では、MacBookにliquidhaskellをインストールする手順をまとめました。

（インストールする対象）

（参考にしたサイト）

実行環境

  • OS: macOS Catalina
  • ghc: version 8.10.7
  • cabal: version 3.6.0.0
Terminal
 electron@diynoMacBook-Pro ~ % cabal update
 electron@diynoMacBook-Pro ~ % ghc -V
The Glorious Glasgow Haskell Compilation System, version 8.10.7
 electron@diynoMacBook-Pro ~ % 
 electron@diynoMacBook-Pro ~ % cabal -V
 cabal-install version 3.6.0.0
compiled using version 3.6.1.0 of the Cabal library
 electron@diynoMacBook-Pro ~ %

SMTゾルバのインストール

１. SMTソルバが必要なので、Z3をbrew installする

Terminal
electron@diynoMacBook-Pro ~ % brew install z3
Terminal
electron@diynoMacBook-Pro ~ % z3 --version
Z3 version 4.8.12 - 64 bit
electron@diynoMacBook-Pro ~ %

（ 参考 ）

LiquidHaskellとはRefinement Typeを用いたHaskell用の検証ツールです。 Refinement Typeとは簡単に言うと、型に述語論理を組み合わせたようなものです。 簡単な具体例を見てみましょう。 以下は0でない整数の型をRefinement Typeを用いて表現したものです。
（ 省略 ）
このように、内包表記によって既存の型に述語論理式を組み合わせて、Haskellの型より細かい型を与えることができます。 特に、Haskellの関数の上に事前条件、事後条件を記述することができるようになり、より厳密な検証を可能にします。 述語論理部分はz3などの、既存のSMTソルバーを用いて検証を行っています。

SMTソルバについては、こちらを参照ください。

LiquidHaskell はバックエンドとして SMT ソルバを使用するため、あらかじめ本体とは別にセットアップしておく必要があります。自分の場合は Z3 の最新版 v4.5.0を選択しました。

SMTソルバの説明の前にまずSATソルバの説明をします。
SATとはsatisfiability problem(充足可能性問題)の略です。
充足可能性問題というのは、一つの命題論理式が与えられたとき、それに含まれる変数の値を偽 (False) あるいは真 (True) にうまく定めることによって全体の値を'真'にできるか、という問題でクラスとしてはNP完全問題になります。
SATソルバは入力として命題論理式を受け取り、式全体の値を'真'にできる(SAT)場合は各変数に対する具体的な真偽値割り当てを出力し、そうでない場合は充足不能(UNSAT)である旨を出力します。

次に、liquidhaskellをインストールします。

１. git cloneでソースをダウンロードする

Terminal
electron@diynoMacBook-Pro ~ % git clone --recursive https://github.com/ucsd-progsys/liquidhaskell.git
fatal: destination path 'liquidhaskell' already exists and is not an empty directory.
electron@diynoMacBook-Pro ~ %

destination path 'liquidhaskell' already exists and is not an empty directory.

  • 過去に --recursiveオプションをつけて実行した際、githubのパスワード入力を求められて、パスワードが見つからなかったことがある。
  • そのとき、--recursiveオプションを外して、git cloneを実行したかもしれない。

__liquidhaskell__ディレクトリの中身を確認

Terminal
electron@diynoMacBook-Pro ~ % ls liquidhaskell
CHANGES.md		Syntax.md		devel			liquid-ghc-prim		scripts			stack.yaml.lock
HLint.hs		TODO.EASY.md		docs			liquid-parallel		shell-stack.nix		syntax
INSTALL.md		TODO.md			exe			liquid-platform		shell.nix		tests
LICENSE			appveyor-copy.bat	external		liquid-prelude		src			tests-by-syntax.md
LICENSE_Z3		appveyor.yml		include			liquid-vector		stack-8.6.5.yaml	typeclass-tests
MIRRORING_MODULES.md	benchmarks		liquid-base		liquidhaskell.cabal	stack-8.6.5.yaml.lock
Makefile		cabal.ghc9.project	liquid-bytestring	mirror-modules		stack-8.8.4.yaml
README.md		cabal.project		liquid-containers	nixpkgs.nix		stack-8.8.4.yaml.lock
Setup.hs		cleanup			liquid-fixpoint		resources		stack.yaml
electron@diynoMacBook-Pro ~ %
  • __tree__コマンドで資源の配置構成を確認
Terminal
electron@diynoMacBook-Pro ~ % tree liquidhaskell 
liquidhaskell
├── CHANGES.md
├── HLint.hs
├── INSTALL.md
├── LICENSE
├── LICENSE_Z3

（ 省略 ）

   │   │   └── Classes.hs
    │   ├── Successors
    │   │   └── Functor.hs
    │   └── Successors.hs
    └── Liquid
        └── ProofCombinators.hs

591 directories, 3701 files
electron@diynoMacBook-Pro ~ %
  • ディレクトリに移動
Terminal
electron@diynoMacBook-Pro ~ % cd liquidhaskell

２. stack installを実行

Terminal
electron@diynoMacBook-Pro liquidhaskell % stack install
Stack looks for packages in the directories configured in
the 'packages' and 'extra-deps' fields defined in your stack.yaml
The current entry points to /Users/electron/liquidhaskell/liquid-fixpoint/,
but no .cabal or package.yaml file could be found there.
electron@diynoMacBook-Pro liquidhaskell %

__no .cabal or package.yaml file could be found there.__というメッセージが吐かれた。
次のウェブサイトに、この事象に対する対処法が書かれている。

no .cabal or package.yaml file could be found #403

Problem:
I get this error when I stack build:

Stack looks for packages in the directories configured in the 'packages' and 'extra-deps' fields >defined in your stack.yaml
The current entry points to unison/yaks/haskeline/ but no .cabal or package.yaml file could be >found there.

Solution:
Use git submodule update --init and then try again;
Alternatively, use git clone --recursive when checking out the project.
  • --recursiveオプションを付けて、git cloneを実行するか、_git submodule update --init_を実行せよ、と書かれている。
  • 過去に --recursiveオプションをつけて実行した際、入力を求められたgithubのパスワードが見つからなくて実行できなかったため、--recursiveオプションを外して、git cloneをしたことがある。

再帰的にダウンロードできていなかった取得漏れの資源を、_git submodule update --init_で取得する。

Terminal
electron@diynoMacBook-Pro liquidhaskell % git submodule update --init
Submodule 'liquid-fixpoint' (https://github.com/ucsd-progsys/liquid-fixpoint.git) registered for path 'liquid-fixpoint'
Cloning into '/Users/electron/liquidhaskell/liquid-fixpoint'...
Submodule path 'liquid-fixpoint': checked out '8b1b48b01a11bd7eed496a09ccc00259388a8799'
electron@diynoMacBook-Pro liquidhaskell %

２'. __stack install__を再実行する

  • 大量のメッセージが吐かれる。処理が進んでいるように見える。
Terminal
electron@diynoMacBook-Pro liquidhaskell % stack install              
Preparing to install GHC to an isolated location.
This will not interfere with any system-level installation.
Downloaded ghc-8.10.2.                                      
xcode-select: error: tool 'xcodebuild' requires Xcode, but active developer directory '/Library/Developer/CommandLineTools' is a command line tools instance
ld: unknown option: --version
ld: unknown option: --version
Configured with: --prefix=/Library/Developer/CommandLineTools/usr --with-gxx-include-dir=/Library/Developer/CommandLineTools/SDKs/MacOSX10.15.sdk/usr/include/c++/4.2.1

（ 省略 ）

liquid-bytestring                > **** LIQUID: SAFE (0 constraints checked) **************************************
liquid-bytestring                > [16 of 16] Compiling Data.ByteString.Unsafe
liquid-bytestring                > 
liquid-bytestring                > **** LIQUID: SAFE (0 constraints checked) **************************************
liquid-bytestring                > 
liquid-bytestring                > copy/register
liquid-bytestring                > Installing library in /Users/electron/liquidhaskell/.stack-work/install/x86_64-osx/9301ab6c5b8601b957b2683d206123d43c11cb4a96d6d95f0d018d5c76d659c0/8.10.2/lib/x86_64-osx-ghc-8.10.2/liquid-bytestring-0.10.10.0-BgHcgfusBA1BP56mKjqzLI
liquid-bytestring                > Registering library for liquid-bytestring-0.10.10.0..
Building all executables for `liquid-platform' once. After a successful build of all of them, only specified executables will be rebuilt.
liquid-platform                  > configure (exe)
liquid-platform                  > Configuring liquid-platform-0.8.10.2...
liquid-platform                  > build (exe)
liquid-platform                  > Preprocessing executable 'liquidhaskell' for liquid-platform-0.8.10.2..
liquid-platform                  > Building executable 'liquidhaskell' for liquid-platform-0.8.10.2..
liquid-platform                  > [1 of 1] Compiling Main
liquid-platform                  > Linking .stack-work/dist/x86_64-osx/Cabal-3.2.0.0/build/liquidhaskell/liquidhaskell ...
liquid-platform                  > copy/register
liquid-platform                  > Installing executable liquidhaskell in /Users/electron/liquidhaskell/.stack-work/install/x86_64-osx/9301ab6c5b8601b957b2683d206123d43c11cb4a96d6d95f0d018d5c76d659c0/8.10.2/bin
Completed 119 action(s).         
Copying from /Users/electron/liquidhaskell/.stack-work/install/x86_64-osx/9301ab6c5b8601b957b2683d206123d43c11cb4a96d6d95f0d018d5c76d659c0/8.10.2/bin/fixpoint to /Users/electron/.local/bin/fixpoint
Copying from /Users/electron/liquidhaskell/.stack-work/install/x86_64-osx/9301ab6c5b8601b957b2683d206123d43c11cb4a96d6d95f0d018d5c76d659c0/8.10.2/bin/liquid to /Users/electron/.local/bin/liquid
Copying from /Users/electron/liquidhaskell/.stack-work/install/x86_64-osx/9301ab6c5b8601b957b2683d206123d43c11cb4a96d6d95f0d018d5c76d659c0/8.10.2/bin/liquidhaskell to /Users/electron/.local/bin/liquidhaskell

Copied executables to /Users/electron/.local/bin:
- fixpoint
- liquid
- liquidhaskell

Warning: Installation path /Users/electron/.local/bin not found on the PATH environment variable.
electron@diynoMacBook-Pro liquidhaskell %

うまく入ったみたい。

Terminal
electron@diynoMacBook-Pro liquidhaskell %  z3 --version
Z3 version 4.8.12 - 64 bit
electron@diynoMacBook-Pro liquidhaskell %

liquidのバージョン確認コマンドが認識された （インストール成功）

Terminal
electron@diynoMacBook-Pro liquidhaskell % stack exec -- liquid --version
LiquidHaskell Version 0.8.10.2.1, Git revision 28a6b51491164f5480778a50f6d83b0f110bfd81 [develop@28a6b51491164f5480778a50f6d83b0f110bfd81 (Wed Oct 20 20:26:54 2021 +0200)] 
Copyright 2013-19 Regents of the University of California. All Rights Reserved.
electron@diynoMacBook-Pro liquidhaskell %

（ 以下の２つは失敗 ）

cabal install liquidhaskellは失敗

Terminal
 electron@diynoMacBook-Pro ~ % cabal install liquidhaskell
 Resolving dependencies...
Build profile: -w ghc-8.10.7 -O1
In order, the following will be built (use -v for more details):
 - Diff-0.3.4 (lib) (requires build)
 - StateVar-1.2.2 (lib) (requires build)
 - base-compat-0.12.0 (lib) (requires build)
 - base-orphans-0.8.5 (lib) (requires build)
 - clock-0.8.2 (lib) (requires build)
 - colour-2.3.6 (lib) (requires build)
 - cmdargs-0.10.21 (lib) (requires build)
 - cereal-0.5.8.1 (lib) (requires build)

 （ 省略 ）
 
 Haskell/Liquid/Types.dyn_o )
[ 54 of 101] Compiling Language.Haskell.Liquid.UX.DiffCheck ( src/Language/Haskell/Liquid/UX/DiffCheck.hs, dist/build/Language/Haskell/Liquid/UX/DiffCheck.o, dist/build/Language/Haskell/Liquid/UX/DiffCheck.dyn_o )
[ 55 of 101] Compiling Language.Haskell.Liquid.UX.Annotate ( src/Language/Haskell/Liquid/UX/Annotate.hs, dist/build/Language/Haskell/Liquid/UX/Annotate.o, dist/build/Language/Haskell/Liquid/UX/Annotate.dyn_o )

src/Language/Haskell/Liquid/UX/Annotate.hs:446:31: error:
    • Couldn't match expected type ‘Key’ with actual type ‘T.Text’
    • In the first argument of ‘(.=)’, namely ‘tshow k’
      In the expression: tshow k .= toJSON a
      In the first argument of ‘object’, namely
        ‘[tshow k .= toJSON a | (k, a) <- M.toList kas]’
    |
446 |   toJSON (Asc kas) = object [ tshow k .= toJSON a | (k, a) <- M.toList kas ]
    |                               ^^^^^^^
cabal: Failed to build liquidhaskell-0.8.10.2 (which is required by exe:liquid
from liquidhaskell-0.8.10.2). See the build log above for details.
electron@diynoMacBook-Pro ~ %

cabal install liquid-platformは依存関係を解決できず。

Terminal
electron@diynoMacBook-Pro ~ % cabal install liquid-platform
Resolving dependencies...
cabal: Could not resolve dependencies:
[__0] trying: liquid-platform-0.8.10.2 (user goal)
[__1] trying: process-1.6.13.2/installed-1.6.13.2 (dependency of
liquid-platform)
[__2] trying: base-4.14.3.0/installed-4.14.3.0 (dependency of process)
[__3] trying: liquid-vector-0.12.1.2 (dependency of liquid-platform)
[__4] next goal: liquid-base (dependency of liquid-platform)
[__4] rejecting: liquid-base-4.15.0.0 (conflict: liquid-vector =>
liquid-base<4.15)
[__4] rejecting: liquid-base-4.14.1.0 (conflict: process =>
base==4.14.3.0/installed-4.14.3.0, liquid-base => base==4.14.1.0)
[__4] rejecting: liquid-base-4.14.0.0 (conflict: liquid-platform =>
liquid-base>=4.14.1.0 && <5)
[__4] fail (backjumping, conflict set: liquid-base, liquid-platform,
liquid-vector, process)
After searching the rest of the dependency tree exhaustively, these were the
goals I've had most trouble fulfilling: base, liquid-base, liquid-platform,
process, liquid-vector
Try running with --minimize-conflict-set to improve the error message.

electron@diynoMacBook-Pro ~ %

liquid-platform-0.9.0.0でバージョン指定しても依存関係解決できず

Terminal
electron@diynoMacBook-Pro ~ % cabal install liquid-platform-0.9.0.0
Resolving dependencies...
cabal: Could not resolve dependencies:
[__0] next goal: liquid-platform (user goal)
[__0] rejecting: liquid-platform-0.8.10.2, liquid-platform-0.8.10.1
(constraint from user target requires ==0.9.0.0)
[__0] fail (backjumping, conflict set: liquid-platform)
After searching the rest of the dependency tree exhaustively, these were the
goals I've had most trouble fulfilling: liquid-platform

electron@diynoMacBook-Pro ~ % cabal update
Downloading the latest package list from hackage.haskell.org
Package list of hackage.haskell.org is up to date at index-state 2021-10-21T21:46:25Z
electron@diynoMacBook-Pro ~ % 
electron@diynoMacBook-Pro ~ % cabal list liquid-platform
* liquid-platform
    Synopsis: A battery-included platform for LiquidHaskell
    Default available version: 0.8.10.2
    Installed versions: [ Unknown ]
    Homepage: https://github.com/ucsd-progsys/liquidhaskell
    License:  BSD3
electron@diynoMacBook-Pro ~ %
1
0
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
Sign upLogin
1
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?