diff --git a/.github/workflows/stan.yml b/.github/workflows/stan.yml new file mode 100644 index 000000000..7933ec41c --- /dev/null +++ b/.github/workflows/stan.yml @@ -0,0 +1,49 @@ +name: stan + +on: + push: + pull_request: + +jobs: + build: + name: ghc ${{ matrix.ghc }} + runs-on: ubuntu-latest + strategy: + matrix: + cabal: ["3.6"] + ghc: + - "8.10.7" + + steps: + - uses: actions/checkout@v2 + with: + submodules: true + + - uses: haskell/actions/setup@v1 + name: Setup GHC and cabal-install + with: + ghc-version: ${{ matrix.ghc }} + cabal-version: ${{ matrix.cabal }} + + - uses: actions/cache@v2 + name: cache ~/.cabal/store + with: + path: ~/.cabal/store + key: ${{ runner.os }}-${{ matrix.ghc }}-cabal + + - uses: pavpanchekha/setup-z3@1.2.2 + name: setup z3 + with: + version: "4.8.7" + + - name: update + run: cabal update + + - name: install stan + run: cabal install stan --installdir=.bin --install-method=copy --overwrite-policy=always + + - name: generate .hie for analysis + run: cabal build liquid-fixpoint:lib:liquid-fixpoint + + - name: stan + run: .bin/stan report \ No newline at end of file diff --git a/.gitignore b/.gitignore index 69429d267..8a5d64aec 100644 --- a/.gitignore +++ b/.gitignore @@ -32,3 +32,6 @@ Session.vim /TAGS /tags *.swp +*.hie +stan.html +.bin/stan diff --git a/.stan.toml b/.stan.toml new file mode 100644 index 000000000..518f79554 --- /dev/null +++ b/.stan.toml @@ -0,0 +1,143 @@ +# Partial: base/head +[[check]] + id = "STAN-0001" + scope = "all" + type = "Exclude" + +# Partial: base/tail +[[check]] + id = "STAN-0002" + scope = "all" + type = "Exclude" + +# Partial: base/init +[[check]] + id = "STAN-0003" + scope = "all" + type = "Exclude" + +# Usage of partial function 'last' for lists +[[check]] + id = "STAN-0004" + scope = "all" + type = "Exclude" + +# Partial: base/!! +[[check]] + id = "STAN-0005" + scope = "all" + type = "Exclude" + +# Partial: base/fromJust +[[check]] + id = "STAN-0008" + scope = "all" + type = "Exclude" + +# Partial: base/read +[[check]] + id = "STAN-0009" + scope = "all" + type = "Exclude" + +# Partial: base/toEnum +[[check]] + id = "STAN-0012" + scope = "all" + type = "Exclude" + +# Partial: base/maximum +[[check]] + id = "STAN-0013" + scope = "all" + type = "Exclude" + +# Partial: base/minimum +[[check]] + id = "STAN-0014" + scope = "all" + type = "Exclude" + +# Partial: base/foldr1 +[[check]] + id = "STAN-0019" + scope = "all" + type = "Exclude" + +# Infinite: base/reverse +[[check]] + id = "STAN-0101" + scope = "all" + type = "Exclude" + +# Infinite: base/isSuffixOf +[[check]] + id = "STAN-0102" + scope = "all" + type = "Exclude" + +# Infinite: base/length +[[check]] + id = "STAN-0103" + scope = "all" + type = "Exclude" + +# Infinite: base/sum +[[check]] + id = "STAN-0105" + scope = "all" + type = "Exclude" + +# Anti-pattern: foldl +[[check]] + id = "STAN-0202" + scope = "all" + type = "Exclude" + +# Data types with non-strict fields +[[check]] + id = "STAN-0206" + scope = "all" + type = "Exclude" + +# Anti-pattern: Slow 'length' for Text +[[check]] + id = "STAN-0208" + scope = "all" + type = "Exclude" + +# Anti-pattern: Slow 'nub' for lists +[[check]] + id = "STAN-0209" + scope = "all" + type = "Exclude" + +# Anti-pattern: unsafe functions +[[check]] + id = "STAN-0212" + scope = "all" + type = "Exclude" + +# Anti-pattern: Pattern matching on '_' +[[check]] + id = "STAN-0213" + scope = "all" + type = "Exclude" + +# Anti-pattern: use 'compare' +[[check]] + id = "STAN-0214" + scope = "all" + type = "Exclude" + +# Missing fixity declaration for operator +[[check]] + id = "STAN-0301" + scope = "all" + type = "Exclude" + +# Using tuples of big size (>= 4) can decrease code readability +[[check]] + id = "STAN-0302" + scope = "all" + type = "Exclude" diff --git a/liquid-fixpoint.cabal b/liquid-fixpoint.cabal index 2fa509184..1e4f8d7c4 100644 --- a/liquid-fixpoint.cabal +++ b/liquid-fixpoint.cabal @@ -153,6 +153,9 @@ library , text , transformers , unordered-containers + ghc-options: + -fwrite-ide-info + -hiedir=.hie if flag(devel) ghc-options: -Werror