diff --git a/.gitignore b/.gitignore index b301fca..a3ae31e 100644 --- a/.gitignore +++ b/.gitignore @@ -1,4 +1,5 @@ -/.direnv/ -/.envrc +.stack-work/ +*~ +.direnv +.envrc *.agdai -/result diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..98e2291 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright Author name here (c) 2024 + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of Author name here nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README.md b/README.md new file mode 100644 index 0000000..fe10660 --- /dev/null +++ b/README.md @@ -0,0 +1 @@ +# wasm-agda diff --git a/Setup.hs b/Setup.hs new file mode 100644 index 0000000..9a994af --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/app/Main.hs b/app/Main.hs new file mode 100644 index 0000000..4c6b30f --- /dev/null +++ b/app/Main.hs @@ -0,0 +1,6 @@ +module Main (main) where + +import Lib + +main :: IO () +main = someFunc diff --git a/default.nix b/default.nix deleted file mode 100644 index f672a6b..0000000 --- a/default.nix +++ /dev/null @@ -1,15 +0,0 @@ -{pkgs ? import {}}: -with pkgs; - agdaPackages.mkDerivation { - pname = "wasm-agda"; - version = "0.0.1"; - - src = pkgs.lib.cleanSource ./.; - everythingFile = "./src/Everything.agda"; - - buildInputs = [ - agdaPackages.standard-library - ]; - - meta = {}; - } diff --git a/package.yaml b/package.yaml new file mode 100644 index 0000000..564fc42 --- /dev/null +++ b/package.yaml @@ -0,0 +1,41 @@ +name: wasm-agda +version: 0.1.0.0 +license: BSD-3-Clause +author: "Aria Shrimpton" +maintainer: "me@aria.rip" +copyright: "2024 Aria Shrimpton" + +extra-source-files: +- README.md + +description: A formalisation of webassembly in agda + +dependencies: +- base >= 4.7 && < 5 +- wasm + +ghc-options: +- -Wall +- -Wcompat +- -Widentities +- -Wincomplete-record-updates +- -Wincomplete-uni-patterns +- -Wmissing-export-lists +- -Wmissing-home-modules +- -Wpartial-fields +- -Wredundant-constraints + +library: + source-dirs: src-lib + +executables: + wasm-agda-exe: + main: Main.hs + source-dirs: app + ghc-options: + - -threaded + - -rtsopts + - -with-rtsopts=-N + dependencies: + - wasm-agda + diff --git a/src-lib/Lib.hs b/src-lib/Lib.hs new file mode 100644 index 0000000..d36ff27 --- /dev/null +++ b/src-lib/Lib.hs @@ -0,0 +1,6 @@ +module Lib + ( someFunc + ) where + +someFunc :: IO () +someFunc = putStrLn "someFunc" diff --git a/stack.yaml b/stack.yaml new file mode 100644 index 0000000..c2aba47 --- /dev/null +++ b/stack.yaml @@ -0,0 +1,9 @@ +resolver: + url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/20/23.yaml + +packages: +- . + +extra-deps: +- wasm-1.1.1@sha256:cea1e6c43d1ee46392eabb6b0f4fc469b6d8b987bcfbdd4694f9c48be346f229,2432 + diff --git a/stack.yaml.lock b/stack.yaml.lock new file mode 100644 index 0000000..0b6ad56 --- /dev/null +++ b/stack.yaml.lock @@ -0,0 +1,20 @@ +# This file was autogenerated by Stack. +# You should not edit this file by hand. +# For more information, please see the documentation at: +# https://docs.haskellstack.org/en/stable/lock_files + +packages: +- completed: + hackage: wasm-1.1.1@sha256:cea1e6c43d1ee46392eabb6b0f4fc469b6d8b987bcfbdd4694f9c48be346f229,2432 + pantry-tree: + sha256: 87029a77cf92dc8ba2b3b20d61563b44b87a4f10c8a3227ff31a2ff2e534cc19 + size: 896 + original: + hackage: wasm-1.1.1@sha256:cea1e6c43d1ee46392eabb6b0f4fc469b6d8b987bcfbdd4694f9c48be346f229,2432 +snapshots: +- completed: + sha256: 4c972e067bae16b95961dbfdd12e07f1ee6c8fffabbfa05c3d65100b03f548b7 + size: 650253 + url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/20/23.yaml + original: + url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/20/23.yaml diff --git a/wasm-agda.cabal b/wasm-agda.cabal new file mode 100644 index 0000000..3f84f6c --- /dev/null +++ b/wasm-agda.cabal @@ -0,0 +1,47 @@ +cabal-version: 2.2 + +-- This file has been generated from package.yaml by hpack version 0.36.0. +-- +-- see: https://github.com/sol/hpack + +name: wasm-agda +version: 0.1.0.0 +description: A formalisation of webassembly in agda +author: Aria Shrimpton +maintainer: me@aria.rip +copyright: 2024 Aria Shrimpton +license: BSD-3-Clause +license-file: LICENSE +build-type: Simple +extra-source-files: + README.md + +library + exposed-modules: + Lib + other-modules: + Paths_wasm_agda + autogen-modules: + Paths_wasm_agda + hs-source-dirs: + src-lib + ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints + build-depends: + base >=4.7 && <5 + , wasm + default-language: Haskell2010 + +executable wasm-agda-exe + main-is: Main.hs + other-modules: + Paths_wasm_agda + autogen-modules: + Paths_wasm_agda + hs-source-dirs: + app + ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N + build-depends: + base >=4.7 && <5 + , wasm + , wasm-agda + default-language: Haskell2010