~omrigan/lalambda-env

ee119b66062cc0426a44f81c0c292221c2dcd085 — Oleg Vasilev 9 months ago
initial
A  => .gitignore +2 -0
@@ 1,2 @@
tla/states
tla/test.out

A  => coq/hello.v +6 -0
@@ 1,6 @@
Require Import Lia.
Lemma eq (x: nat) : x=x.
Proof.
    auto.
Qed.
Print eq.
\ No newline at end of file

A  => haskell/.gitignore +2 -0
@@ 1,2 @@
.stack-work/
*~
\ No newline at end of file

A  => haskell/ChangeLog.md +3 -0
@@ 1,3 @@
# Changelog for haskell

## Unreleased changes

A  => haskell/LICENSE +30 -0
@@ 1,30 @@
Copyright Author name here (c) 2021

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.

A  => haskell/README.md +1 -0
@@ 1,1 @@
# haskell

A  => haskell/Setup.hs +2 -0
@@ 1,2 @@
import Distribution.Simple
main = defaultMain

A  => haskell/app/Main.hs +18 -0
@@ 1,18 @@
import Data.Char
import Data.Hashable
import System.IO
myHash :: String -> Int
myHash str = hash (dropWhile isSpace str)


promptLine :: String -> IO String
promptLine prompt = do
    putStr prompt
    hFlush stdout
    getLine

main :: IO ()
main = do
    line1 <- promptLine "Coq the lemma used by auto (eq_****): "           
    line2 <- promptLine "TLA a total number of states: "                 
    putStrLn (show (myHash (line1 ++ line2)))

A  => haskell/haskell.cabal +65 -0
@@ 1,65 @@
cabal-version: 1.12

-- This file has been generated from package.yaml by hpack version 0.33.0.
--
-- see: https://github.com/sol/hpack
--
-- hash: 12806a3fe9f5c80383f05a6c37b404225ee27954b06b84eba0f1210191366e9c

name:           haskell
version:        0.1.0.0
description:    Please see the README on GitHub at <https://github.com/githubuser/haskell#readme>
homepage:       https://github.com/githubuser/haskell#readme
bug-reports:    https://github.com/githubuser/haskell/issues
author:         Author name here
maintainer:     example@example.com
copyright:      2021 Author name here
license:        BSD3
license-file:   LICENSE
build-type:     Simple
extra-source-files:
    README.md
    ChangeLog.md

source-repository head
  type: git
  location: https://github.com/githubuser/haskell

library
  exposed-modules:
      Lib
  other-modules:
      Paths_haskell
  hs-source-dirs:
      src
  build-depends:
      base >=4.7 && <5
    , hashable
  default-language: Haskell2010

executable haskell-exe
  main-is: Main.hs
  other-modules:
      Paths_haskell
  hs-source-dirs:
      app
  ghc-options: -threaded -rtsopts -with-rtsopts=-N
  build-depends:
      base >=4.7 && <5
    , hashable
    , haskell
  default-language: Haskell2010

test-suite haskell-test
  type: exitcode-stdio-1.0
  main-is: Spec.hs
  other-modules:
      Paths_haskell
  hs-source-dirs:
      test
  ghc-options: -threaded -rtsopts -with-rtsopts=-N
  build-depends:
      base >=4.7 && <5
    , hashable
    , haskell
  default-language: Haskell2010

A  => haskell/package.yaml +49 -0
@@ 1,49 @@
name:                haskell
version:             0.1.0.0
github:              "githubuser/haskell"
license:             BSD3
author:              "Author name here"
maintainer:          "example@example.com"
copyright:           "2021 Author name here"

extra-source-files:
- README.md
- ChangeLog.md

# Metadata used when publishing your package
# synopsis:            Short description of your package
# category:            Web

# To avoid duplicated efforts in documentation and dealing with the
# complications of embedding Haddock markup inside cabal files, it is
# common to point users to the README.md file.
description:         Please see the README on GitHub at <https://github.com/githubuser/haskell#readme>

dependencies:
- base >= 4.7 && < 5
- hashable

library:
  source-dirs: src

executables:
  haskell-exe:
    main:                Main.hs
    source-dirs:         app
    ghc-options:
    - -threaded
    - -rtsopts
    - -with-rtsopts=-N
    dependencies:
    - haskell

tests:
  haskell-test:
    main:                Spec.hs
    source-dirs:         test
    ghc-options:
    - -threaded
    - -rtsopts
    - -with-rtsopts=-N
    dependencies:
    - haskell

A  => haskell/src/Lib.hs +2 -0
@@ 1,2 @@
module Lib
    ( ) where

A  => haskell/stack.yaml +68 -0
@@ 1,68 @@
# This file was automatically generated by 'stack init'
#
# Some commonly used options have been documented as comments in this file.
# For advanced use and comprehensive documentation of the format, please see:
# https://docs.haskellstack.org/en/stable/yaml_configuration/

# Resolver to choose a 'specific' stackage snapshot or a compiler version.
# A snapshot resolver dictates the compiler version and the set of packages
# to be used for project dependencies. For example:
#
# resolver: lts-3.5
# resolver: nightly-2015-09-21
# resolver: ghc-7.10.2
#
# The location of a snapshot can be provided as a file or url. Stack assumes
# a snapshot provided as a file might change, whereas a url resource does not.
#
# resolver: ./custom-snapshot.yaml
# resolver: https://example.com/snapshots/2018-01-01.yaml
resolver:
  url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/9.yaml

# User packages to be built.
# Various formats can be used as shown in the example below.
#
# packages:
# - some-directory
# - https://example.com/foo/bar/baz-0.0.2.tar.gz
#   subdirs:
#   - auto-update
#   - wai
packages:
- .
# Dependency packages to be pulled from upstream that are not in the resolver.
# These entries can reference officially published versions as well as
# forks / in-progress versions pinned to a git hash. For example:
#
# extra-deps:
# - acme-missiles-0.3
# - git: https://github.com/commercialhaskell/stack.git
#   commit: e7b331f14bcffb8367cd58fbfc8b40ec7642100a
#
extra-deps:
 - hashable-1.3.1.0

# Override default flag values for local packages and extra-deps
# flags: {}

# Extra package databases containing global packages
# extra-package-dbs: []

# Control whether we use the GHC we find on the path
# system-ghc: true
#
# Require a specific version of stack, using version ranges
# require-stack-version: -any # Default
# require-stack-version: ">=2.5"
#
# Override the architecture used by stack, especially useful on Windows
# arch: i386
# arch: x86_64
#
# Extra directories used by stack for building
# extra-include-dirs: [/path/to/dir]
# extra-lib-dirs: [/path/to/dir]
#
# Allow a newer minor version of GHC than the snapshot specifies
# compiler-check: newer-minor

A  => haskell/stack.yaml.lock +20 -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: hashable-1.3.1.0@sha256:d965e098e06cc585b201da6137dcb31c40f35eb7a937b833903969447985c076,3784
    pantry-tree:
      size: 937
      sha256: 8ea12ecf91a4d6fd1f1f885faec1b3eeb4baa0db27ccff49072cfdd0c15833ba
  original:
    hackage: hashable-1.3.1.0
snapshots:
- completed:
    size: 567037
    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/9.yaml
    sha256: d7d8d5106e53d1669964bd8bd2b0f88a5ad192d772f5376384b76738fd992311
  original:
    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/9.yaml

A  => haskell/test/Spec.hs +2 -0
@@ 1,2 @@
main :: IO ()
main = putStrLn "Test suite not yet implemented"

A  => readme.md +24 -0
@@ 1,24 @@
# Настройка окружения

## Coq
Установите https://github.com/coq/platform/

### Редакторы
Дима советует: заведите VSCode + VSCoq.
Антон советует: пользуйте Emacs + Proof General.
Олег бурчит: если ничего не работает, сработает CoqIDE.

## TLA
Установите https://adoptopenjdk.net/ java16 должны работать

### Редакторы
Дима говорит: рекомендуется VSCode. Сгодится TLA+ Toolbox.

## Haskell
Установите stack

# Сдача контеста
 - Верифицируйте лемму из coq/hello.v. Посмотрите в выводе через какую лемму была доказана наша лемма
 - Сделайте model checking у модели из tla. Посмотрите в выводе сколько всего состояний было использовано
 - Запустите stack run в папке haskell. Введите полученные на предыдущих шагах значения. Выведенное число и есть ваш ответ на контест


A  => tla/test.cfg +15 -0
@@ 1,15 @@
\* SPECIFICATION
\* Uncomment the previous line and provide the specification name if it's declared
\* in the specification file. Comment INIT / NEXT parameters if you use SPECIFICATION.

CONSTANTS
    greeting = "Hello"

INIT Init
NEXT Next

\* PROPERTY
\* Uncomment the previous line and add property names

\* INVARIANT
\* Uncomment the previous line and add invariant names

A  => tla/test.tla +35 -0
@@ 1,35 @@
---- MODULE test ----
EXTENDS TLC

(* --algorithm hello_world
variable s \in {"Hello", "World!"};
begin
  A:
    print s;
end algorithm; *)
\* BEGIN TRANSLATION (chksum(pcal) = "c66c1fcc" /\ chksum(tla) = "e102bc6a")
VARIABLES s, pc

vars == << s, pc >>

Init == (* Global variables *)
        /\ s \in {"Hello", "World!"}
        /\ pc = "A"

A == /\ pc = "A"
     /\ PrintT(s)
     /\ pc' = "Done"
     /\ s' = s

(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == pc = "Done" /\ UNCHANGED vars

Next == A
           \/ Terminating

Spec == Init /\ [][Next]_vars

Termination == <>(pc = "Done")

\* END TRANSLATION 
====