MacBookにliquidhaskellをインストール

データ型が持つことが許される値の範囲を定義したり（依存型 __*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をインストールする手順をまとめました。

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

- [Hackage liquid-platform: A battery-included platform for LiquidHaskell](https://hackage.haskell.org/package/liquid-platform)
- [ucsd-progsys/liquidhaskellInstall LiquidHaskell](https://github.com/ucsd-progsys/liquidhaskell/blob/develop/INSTALL.md)

##（参考にしたサイト）

- [LiquidHaskell のインストールと学習方法](https://haskell.e-bigmoon.com/posts/2018/03-03-liquidhaskell-intro.html)
- [Windows10でHaskell開発環境構築](https://qiita.com/kitsukitsuki/items/a56cbfc0decd09c16248)

##実行環境

- OS: macOS Catalina
- ghc: version 8.10.7
- cabal: version 3.6.0.0

```bash: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する

```bash:Terminal
electron@diynoMacBook-Pro ~ % brew install z3
```

```bash:Terminal
electron@diynoMacBook-Pro ~ % z3 --version
Z3 version 4.8.12 - 64 bit
electron@diynoMacBook-Pro ~ % 
```

####__（ 参考 ）__

- [LiquidHaskell 入門 その1](https://forestaa.github.io/blog/posts/liquidhaskell1/)

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

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

- [LiquidHaskell コトハジメ](https://ccvanishing.hateblo.jp/entry/2016/12/24/193038)
> LiquidHaskell はバックエンドとして SMT ソルバを使用するため、あらかじめ本体とは別にセットアップしておく必要があります。自分の場合は Z3 の最新版 v4.5.0を選択しました。

- [SAT/SMTソルバを自作してみる話](https://rkx1209.hatenablog.com/entry/2017/12/17/175439)
> SMTソルバの説明の前にまずSATソルバの説明をします。
> SATとはsatisfiability problem(充足可能性問題)の略です。
> 充足可能性問題というのは、一つの命題論理式が与えられたとき、それに含まれる変数の値を偽 (False) あるいは真 (True) にうまく定めることによって全体の値を'真'にできるか、という問題でクラスとしてはNP完全問題になります。
> SATソルバは入力として命題論理式を受け取り、式全体の値を'真'にできる(SAT)場合は各変数に対する具体的な真偽値割り当てを出力し、そうでない場合は充足不能(UNSAT)である旨を出力します。
- [SAT/SMTソルバの仕組み](https://www.slideshare.net/sakai/satsmt)

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

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

```bash: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*__ディレクトリの中身を確認

```bash: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*__コマンドで資源の配置構成を確認

```bash: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 ~ %
```

* ディレクトリに移動

```bash:Terminal
electron@diynoMacBook-Pro ~ % cd liquidhaskell
```

###２. *stack install*を実行

```bash: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.*__というメッセージが吐かれた。
次のウェブサイトに、この事象に対する対処法が書かれている。

https://github.com/unisonweb/unison/issues/403

>no .cabal or package.yaml file could be found #403
>
>```text:
> 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**_で取得する。

```bash: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*__を再実行する

- 大量のメッセージが吐かれる。処理が進んでいるように見える。

```bash: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 % 
```

####うまく入ったみたい。

https://forestaa.github.io/blog/posts/liquidhaskell1/

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


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

```bash: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は失敗

```bash: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は依存関係を解決できず。

```bash: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でバージョン指定しても依存関係解決できず

```bash: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 ~ %
```