Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Tutorial on the protocol anatomy and tests #596

Merged
merged 17 commits into from
Feb 3, 2023
Merged

Tutorial on the protocol anatomy and tests #596

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
279b683
make the example even more interesting
konnov Jan 31, 2023
038ba51
Merge branch 'main' of github.com:informalsystems/quint
konnov Jan 31, 2023
aad215c
starting the tutorial 3
konnov Jan 31, 2023
9f1571d
the large chunk of the tutorial
konnov Jan 31, 2023
6cd3e49
finished the tutorial
konnov Feb 1, 2023
b4ea2c1
small fixes
konnov Feb 1, 2023
75df3e2
update the readme files
konnov Feb 1, 2023
60a873c
add links to SDK and Cosmwasm
konnov Feb 1, 2023
eade4a6
Merge branch 'main' into igor/tutorial522-2
konnov Feb 1, 2023
bd8a501
Language fixes
thpani Feb 2, 2023
d885df8
Apply suggestions from code review
konnov Feb 3, 2023
61d963c
address the comments
konnov Feb 3, 2023
4a104f7
add a symbolic link to the tutorial
konnov Feb 3, 2023
1ce8a3d
fix the tests and fixing a few comments
konnov Feb 3, 2023
c0449eb
Merge branch 'main' into igor/tutorial522-2
konnov Feb 3, 2023
f36a15b
fix the tests and comments
konnov Feb 3, 2023
08c6d1a
Merge branch 'igor/tutorial522-2' of github.com:informalsystems/quint…
konnov Feb 3, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 12 additions & 12 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -97,11 +97,11 @@ completely implementing every pass.
| :--------------- | :----: | :-------------: | :-----: | :----------: | :-------: | :---------: | :-------: |
| [Booleans][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: | :white_check_mark: |
| [Integers][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: | :white_check_mark: |
| [if-then-else][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: | :x: |
| [Operator definitions][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: | :x: |
| [Modes][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: [234][] | :x: | :x: |
| [if-then-else][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: | :white_check_mark: |
| [Operator definitions][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: | :white_check_mark: |
| [Modes][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: [234][] | :x: | :white_check_mark: |
| [Sets][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark:/:x: [238][] | :x: | :x: |
| [Guess][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: | :x: |
| [nondet][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: | :white_check_mark: |
| [Maps][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: | :x: |
| [Lists][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: | :x: |
| [Records][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: | :x: |
Expand All @@ -112,19 +112,19 @@ completely implementing every pass.
| [Module instances][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: [237][] | :x: | :x: |
| [Multiple files][] | :x: [8][] | :x: | :x: | :x: | :x: | :x: | :x: |
| [Constant declarations][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: [236][] | :x: | :x: |
| [Variable definitions][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: | :x: |
| [Variable definitions][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: | :white_check_mark: |
| [Assumptions][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: | :x: [235][] | :x: | :x: |
| [Lambdas][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: | :x: |
| [Lambdas][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: | :white_check_mark: |
| [Multiline disjunctions][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: | :x: |
| [Multiline conjunctions][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: | :x: |
| [Delayed assignment][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: | :x: |
| Invariant checking | - | - | | | :white_check_mark: | :x: | :x: |
| [Multiline conjunctions][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: | :white_check_mark: |
| [Delayed assignment][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: | :white_check_mark: |
| Invariant checking | - | - | | | :white_check_mark: | :x: | :white_check_mark: |
| [Higher-order definitions][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: [221][] | :x: | :x: |
| [Runs][] | :white_check_mark: | :white_check_mark: | :x: | :x: | :white_check_mark: | :x: | :x: |
| [Runs][] | :white_check_mark: | :white_check_mark: | :x: | :x: | :white_check_mark: | :x: | :white_check_mark: |
| [Temporal operators][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | *non-goal* | :x: | :x: |
| [Fairness][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | *non-goal* | :x: | :x: |
| [Unbounded quantifiers][] | :white_check_mark: | :white_check_mark: | :x: | :x: | *non-goal* | :x: | :x: |
| [String literals][], see #118 | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: | :x: |
| [String literals][], see #118 | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: | :white_check_mark: |
| ~~uninterpreted types~~, see #118 | :white_check_mark: | :white_check_mark: | :x: | :x: | :x: | :x: | :x: |


Expand All @@ -146,7 +146,7 @@ completely implementing every pass.
[Multiline disjunctions]: ./doc/lang.md#multiline-disjunctions
[Multiline conjunctions]: ./doc/lang.md#multiline-conjunctions
[if-then-else]: ./doc/lang.md#condition
[Guess]: ./doc/lang.md#existential-quantifier-and-non-deterministic-choice
[nondet]: ./doc/lang.md#existential-quantifier-and-non-deterministic-choice
[Maps]: ./doc/lang.md#maps-aka-functions
[Records]: ./doc/lang.md#records
[Discriminated unions]: ./doc/lang.md#discriminated-unions
Expand Down
1 change: 1 addition & 0 deletions examples/solidity/Coin/coin.qnt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
../../../tutorials/lesson3-anatomy/coin.qnt
6 changes: 3 additions & 3 deletions quint/cli-tests.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -192,10 +192,10 @@ Temporarily disabled.
<!-- !test check counters - Types & Effects-->
quint typecheck ../examples/language-features/counters.qnt

### OK on typecheck Coin
### OK on typecheck coin

<!-- !test check Coin - Types & Effects-->
quint typecheck ../examples/solidity/Coin/Coin.qnt
<!-- !test check coin - Types & Effects-->
quint typecheck ../examples/solidity/Coin/coin.qnt

### OK on typecheck SimpleAuctionNonComposable.qnt

Expand Down
3 changes: 2 additions & 1 deletion tutorials/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,8 @@
# Compile all Quint tutorials
tutorials: lesson0-helloworld/hello.qnt \
lesson1-booleans/booleans.qnt \
lesson2-integers/integers.qnt
lesson2-integers/integers.qnt \
lesson3-anatomy/coin.qnt
@echo "Updated all tutorials"

%.qnt: %.template.qnt
Expand Down
5 changes: 3 additions & 2 deletions tutorials/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,11 +13,12 @@ These tutorials are currently available in the classic format:
- [Hello, world!](./lesson0-helloworld/hello.md)
- [Tutorial on Booleans](./lesson1-booleans/booleans.md)
- [Tutorial on integers](./lesson2-integers/integers.md)
- [Tutorial on basic protocol anatomy and tests](./lesson3-integers/coin.md)

## 2. CodeTour tutorials

If you like interactive language tutorials, we have recorded a few using
[CodeTour][]. You have to install two extensions:
If you like interactive language tutorials, we have recorded the above listed
tutorials using [CodeTour][]. You have to install two extensions:

- [Quint VSCode][] is our language extension,
- [CodeTour][] is the extension of replaying code tutorials.
Expand Down
Loading