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 |