Updated on 2022-06-10 10:15:21 UTC
refreshed every 30 minutes

@clarus1Guillaume Claret's actions (99)

Resource Action Why
tezos/tezos#1072
Follow-up from "Proto: Use saturated arithmetic to represent gas": Coq-of-ocaml / Property-based testing of `saturation_repr.ml`
coq-of-ocaml ๐Ÿ” proto test โš’ tests::crowbar
Complete task clarus1 is assigned
tezos/tezos#1141
Integrate Coq-Tezos-of-OCaml repo into Tezos
coq-of-ocaml ๐Ÿ” tests::crowbar
Solve issue clarus1 is assigned
tezos/tezos#1484
Protocol env coq-of-ocaml check ๐Ÿ”
CI โš™ coq-of-ocaml ๐Ÿ” proto::environment triage::level2 type::feature
Solve issue clarus1 is assigned
tezos/tezos#1520
Report stack overflow error in Coq itself for the protocol ๐Ÿ”
coq-of-ocaml ๐Ÿ” state::to-do triage::level2
Solve issue clarus1 is assigned
tezos/tezos#1541
Remove all the exceptions from the protocol
Code quality ๐ŸŒŸ coq-of-ocaml ๐Ÿ” good beginner task ๐Ÿผ Nice to have ๐Ÿ‘ถ proto state::to-do triage::level2
Solve issue clarus1 is assigned
tezos/tezos!3303
Draft: Ongoing branch with changes to compile the protocol to Coq ๐Ÿ”
coq-of-ocaml ๐Ÿ” proto type::meta
UnWIP clarus1 is the original author
tezos/tezos!4258
Draft: Proto: fix protocol name in coq-of-ocaml config
coq-of-ocaml ๐Ÿ” proto
UnWIP clarus1 is the original author
arvidnl/tezos_coredev_dashboard!44
Add front draft
Fix CI clarus1 is the original author and triggered last pipeline
Add a merge-team reviewer clarus1 is the original author
Wait for pipeline clarus1 is the original author
nomadic-labs/coq-tezos-of-ocaml!508
Draft: Carbonated maps
Blocking nomadic-labs/coq-tezos-of-ocaml#127
Close or reply to thread clarus1 is the thread author
nomadic-labs/mi-cho-coq!151
Fix #66 and #67
bug test
Review or approve clarus1 is assigned
nomadic-labs/coq-tezos-of-ocaml!548
More simulation cases for the interpreter
michelson
Review or approve clarus1 is assigned
Add a merge-team reviewer clarus1 is the original author
nomadic-labs/mi-cho-coq!113
Replace String.string_dec by String.eqb in Dexter 2
Fix CI clarus1 is the original author and triggered last pipeline
Add a merge-team reviewer clarus1 is the original author
nomadic-labs/mi-cho-coq!57
Integrate the output of coq-of-ocaml with the interpreter
coq-of-ocaml ๐Ÿ“
Add a merge-team reviewer clarus1 is the original author
nomadic-labs/coq-tezos-of-ocaml#117
Define all remaining cases for dep_step
michelson sprint-3 sprint-4
Complete task clarus1 is assigned
nomadic-labs/tezos#349
nomadic-labs/tezos#349
tests
Solve issue clarus1 is assigned
nomadic-labs/mi-cho-coq#3
nomadic-labs/mi-cho-coq#3
coq-of-ocaml ๐Ÿ“ Doing
Solve issue clarus1 is assigned
nomadic-labs/coq-tezos-of-ocaml#71
Verify the non-iterable data stores
storage
Solve issue clarus1 is assigned
nomadic-labs/coq-tezos-of-ocaml#94
Encodings in ๐Ÿ—๏ธ Apply_results.v
data-encoding
Complete task clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#52
Follow-up from "implementing gadt-style opcodes"
Complete task clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#105
Encodings in ๐Ÿฆ Sc_rollup_inbox_repr.v
data-encoding
Complete task clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#160
Improve the translation of asserts
coq-of-ocaml internal errors
Complete task clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#163
Have a tactic to remove asserts
internal errors
Complete task clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#37
Update autounfold rules for integers
Complete task clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#38
Follow-up from "Resolve "Add correct compare definitions""
Complete task clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#47
Non-termination in script_string_repr
Complete task clarus1 opened issue and no one is assigned
nomadic-labs/tezos#270
nomadic-labs/tezos#270
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/mi-cho-coq#64
Types in OCaml and not in Mi-Cho-Coq
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#24
Have automated tactics for RPC_arg
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#40
Optimize proofs in Apply_results
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#43
Remove imperative updates from the generated Coq
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#44
Add utils in the environment
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#45
Remove unused existential variables in casts
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#46
Enforce line limit of 80 characters in the CI
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#49
Upgrade to Coq 8.15
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#50
Define String.length in int
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#62
Verify ๐Ÿ”ฅ Carbonated_map.v
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#65
Translate the data-encoding library to Coq
coq-of-ocaml data-encoding
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#66
Represent the effects of the data-encoding library
coq-of-ocaml data-encoding
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#67
Specify the data-encoding library
data-encoding
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#68
Verify the data-encoding library
data-encoding
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#69
Sync the data-encoding spec of the environment to the library
data-encoding
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#70
Check the equality of dep_step for axioms
michelson
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#90
Verify `back_path_is_valid` for skip lists
skip-lists sprint-3 sprint-4
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#91
Verify `back_path_is_uniq` for skip lists
skip-lists
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#118
Terminate the proof of dep_step_eq
michelson sprint-3 sprint-4
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#129
Remove the warnings from coq-of-ocaml
cleaning
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#150
Translate test_gas_properties.ml
coq-of-ocaml tests
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#151
Translate test_merkle_list.ml
coq-of-ocaml tests
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#152
Translate test_sampler.ml
coq-of-ocaml tests
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#153
Translate test_script_comparison.ml
coq-of-ocaml tests
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#159
Remove one patch.rb item
coq-of-ocaml
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#165
Have lint rule to forbid trailing spaces
cleaning coq-of-ocaml
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#175
Verify test_to_list_of_list_proof
tests
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#176
Verify test_empty_left_identity_for_merge_proof
tests
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#177
Verify test_empty_right_identity_for_merge_proof
tests
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#178
Verify test_size_merge_self_proof
tests
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#179
Verify test_size_add_one_proof
tests
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#180
Verify test_size_remove_one_proof
tests
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#181
Verify test_merge_against_list_proof
tests
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#182
Verify test_merge_overlaps_left_proof
tests
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#183
Verify test_merge_overlaps_right_proof
tests
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#184
Verify test_merge_overlaps_add_proof
tests
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#185
Verify test_merge_fail_proof
tests
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#186
Verify test_merge_map_keep_existing_proof
tests
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#187
Verify test_merge_map_replace_existing_proof
tests
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#188
Verify test_find_non_existing_proof
tests
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#189
Verify test_find_existing_proof
tests
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#190
Verify test_update_add_proof
tests
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#191
Verify test_update_merge_proof
tests
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#192
Verify test_update_delete_proof
tests
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#193
Verify test_map_proof
tests
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#194
Verify test_fold_empty_proof
tests
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#195
Verify test_fold_proof
tests
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#196
Verify test_fold_to_list_proof
tests
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#197
Verify test_map_fail_proof
tests
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#200
Saturation: Verify tests_add_proof
tests
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#201
Saturation: Verify tests_mul_proof
tests
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#202
Saturation: Verify test_add_commutes_proof
tests
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#203
Saturation: Verify tests_sub_proof
tests
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#204
Saturation: Verify tests_add_sub_proof
tests
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#205
Saturation: Verify tests_boundaries_proof
tests
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml#206
Definition the simulation of the IView instruction
michelson
Solve issue clarus1 opened issue and no one is assigned
nomadic-labs/coq-tezos-of-ocaml!403
Draft: Verify non iterable indexable data storages
Fix CI clarus1 is the original author and triggered last pipeline
UnWIP clarus1 is the original author
nomadic-labs/coq-tezos-of-ocaml!483
Draft: Sc_rollup_inbox_proof_encodings
Fix CI clarus1 triggered last pipeline
nomadic-labs/coq-tezos-of-ocaml!536
Draft: More simulation interpreter proofs using Valid predicate
michelson
Fix CI clarus1 is the original author and triggered last pipeline
UnWIP clarus1 is the original author
nomadic-labs/coq-tezos-of-ocaml!564
Draft: Simulation for the transfer function
michelson
Fix CI clarus1 is the original author and triggered last pipeline
UnWIP clarus1 is the original author
nomadic-labs/coq-tezos-of-ocaml!291
Draft: 96-parse-unparse-comparable_data
Close or reply to thread clarus1 is the thread author
nomadic-labs/coq-tezos-of-ocaml!379
Draft: Storage: verify the carbonated indexed storage functor
Fix CI clarus1 is the original author and triggered last pipeline
UnWIP clarus1 is the original author
nomadic-labs/mi-cho-coq!52
WIP: Beginning of import of the evaluation function
coq-of-ocaml ๐Ÿ“
UnWIP clarus1 is the original author
nomadic-labs/data-encoding!58
Draft: binary lexeme backend for coq - with Coq translation
UnWIP clarus1 is the original author
nomadic-labs/coq-tezos-of-ocaml!524
Draft: Simulation of parse_instr
michelson
UnWIP clarus1 is the original author

Repositories

arvidnl/tezos_coredev_dashboardarvidnl/tezos_coredev_dashboard

Dispatchers:   @arvidnlarvidnl (from project owners)
Merge‑teamers:   @arvidnlarvidnl (copied from dispatchers)
Issue watchers:  No one (no one)
Labels:  CI UI Workflow

nomadic-labs/coq-tezos-of-ocamlnomadic-labs/coq-tezos-of-ocaml

Issue watchers:  No one (no one)

dnomadic-labs/data-encoding

Issue watchers:  No one (no one)

Mnomadic-labs/mi-cho-coq

Issue watchers:  No one (no one)

nomadic-labs/tezosnomadic-labs/tezos

Issue watchers:  No one (no one)

tezos/tezostezos/tezos

Dispatchers:   @arvidnlarvidnl (from issue tezos/tezos#1062)
Issue watchers:  No one (from issue tezos/tezos#1061)
Labels:  priority::critical type::incident type::bug priority::high type::flake priority::medium confirmed ๐Ÿ‘ alpha ฮฑ approved arm64 bad UX ๐ŸŽ baking bootstrap build system CI โš™ ci--arm64 ci--docker ci--docs ci--no-coverage ci--opam client ๐Ÿง Code quality ๐ŸŒŸ compiler ๐Ÿค– coq-of-ocaml ๐Ÿ” crypto DAL dalphanet deps-rework doc ๐Ÿ“– doc-only docker ๐Ÿณ dune3 emacs encoding error-handling gas ๐Ÿš‚ good beginner task ๐Ÿผ incident javascript ledger light ๐Ÿ’ก liquidity-baking lmdb logging lwt โžก๏ธ mainnet-only mandatory marge-priority::high mempool michelson โš— minor mockup monad-wrangling monitoring multisig needs help needs testing Nice to have ๐Ÿ‘ถ node ๐Ÿ–ฅ Not for V1 ๐Ÿ’ซ ode-observability opam opsec ๐Ÿ” p2p ๐ŸŒ Packaging ๐Ÿ“ฆ performance platform-compatibility priority::low proto proto::Consensus algorithm proto::environment proto::next proto::plugins proxy python ๐Ÿ ready for review party ๐ŸŽ‰ release manager ๐Ÿ‘ท Release Process Crew revert rpc โ˜Ž rust sapling scoru security shell signer simple snoop specification state::blocked state::in-progress state::in-review state::ready-to-merge state::to-do stdlib storage support ๐Ÿ’ team::michelson team::node-tools team::SDK Terraform test โš’ testnet::idiazabalnet tests::alcotest tests::CI tests::coverage tests::crowbar tests::documentation tests::flextesa tests::performance tests::pytest tests::qcheck tests::suite tests::tezt tickets tooling toru::client toru::daemon ๐Ÿ‘น toru::layer1 toru::layer1+2 toru::layer2 toru::storage ๐ŸŒณ triage::level0 triage::level1 triage::level2 try-reproduce type::benchmark type::discussion type::feature type::meta type::suggestion validation waiting for feedback wasm-pvm:lazy-tree wontfix ๐Ÿ™ˆ wrapper-shell-script