Updated on 2022-06-10 10:15:33 UTC
refreshed every 30 minutes
refreshed every 30 minutes
clarus1 (79)
webmathew (18)
dhilst (13)
deepmindster (12)
emarzion (11)
RektYuan (8)
kewersonhugo (8)
MBourgoin (7)
OanaLP (7)
SamREye (7)
davdumas (7)
jgonlabs (7)
klakplok (7)
nguyencharles.nlabs (7)
onurb (7)
pirbo (7)
raphael-proust (7)
romain.nl (7)
vbotbol (7)
kumar.shubham.off (5)
jorisptrs (3)
tudoroscoiu (2)
TinoAlfie (1)Everybody's actions on nomadic-labs/coq-tezos-of-ocaml (167)
| Resource | Action | Who and why |
|---|---|---|
| nomadic-labs/coq-tezos-of-ocaml!560 encoding Blocking nomadic-labs/coq-tezos-of-ocaml#102 nomadic-labs/coq-tezos-of-ocaml#101 | Reply to thread |
webmathew
is the original author |
| Reply to thread |
webmathew
is the original author |
|
| Add a merge-team reviewer |
webmathew
is the original author |
|
| Help add merge-team reviewers |
davdumas
jgonlabs
klakplok
MBourgoin
nguyencharles.nlabs
OanaLP
onurb
pirbo
raphael-proust
romain.nl
SamREye
vbotbol
is a dispatcher |
|
| nomadic-labs/coq-tezos-of-ocaml!508 Draft: Carbonated maps Blocking nomadic-labs/coq-tezos-of-ocaml#127 | Reply to thread |
emarzion
is the original author |
| Reply to thread |
emarzion
is the original author |
|
| Reply to thread |
emarzion
is the original author |
|
| Reply to thread |
emarzion
is the original author |
|
| Reply to thread |
emarzion
is the original author |
|
| Reply to thread |
emarzion
is the original author |
|
| Reply to thread |
emarzion
is the original author |
|
| Close or reply to thread |
clarus1
is the thread author |
|
| UnWIP |
emarzion
is the original author |
|
| nomadic-labs/coq-tezos-of-ocaml!504 Draft: dep_merge_branches_eq Simulations 20-29 Blocking nomadic-labs/coq-tezos-of-ocaml#135 | Fix CI |
webmathew
is the original author |
|
deepmindster
triggered last pipeline |
||
| UnWIP |
webmathew
is the original author |
|
| nomadic-labs/coq-tezos-of-ocaml!510 MR for saturation fuzzing proofs help | Reply to thread |
jorisptrs
is the original author |
| Fix CI |
jorisptrs
is the original author and triggered last pipeline |
|
| Add a merge-team reviewer |
jorisptrs
is the original author |
|
| Close or reply to thread |
deepmindster
is the thread author |
|
| Close or reply to thread |
deepmindster
is the thread author |
|
| Help add merge-team reviewers |
davdumas
jgonlabs
klakplok
MBourgoin
nguyencharles.nlabs
OanaLP
onurb
pirbo
raphael-proust
romain.nl
SamREye
vbotbol
is a dispatcher |
|
| nomadic-labs/coq-tezos-of-ocaml!563 Added simulation for dep_big_map_get_by_hash | Reply to thread |
RektYuan
is the original author |
| Add a merge-team reviewer |
RektYuan
is the original author |
|
| Help add merge-team reviewers |
davdumas
jgonlabs
klakplok
MBourgoin
nguyencharles.nlabs
OanaLP
onurb
pirbo
raphael-proust
romain.nl
SamREye
vbotbol
is a dispatcher |
|
| nomadic-labs/coq-tezos-of-ocaml!568 Added proofs for index_opt_eq and substr_l_eq | Reply to thread |
RektYuan
is the original author |
| Add a merge-team reviewer |
RektYuan
is the original author |
|
| Help add merge-team reviewers |
davdumas
jgonlabs
klakplok
MBourgoin
nguyencharles.nlabs
OanaLP
onurb
pirbo
raphael-proust
romain.nl
SamREye
vbotbol
is a dispatcher |
|
| nomadic-labs/coq-tezos-of-ocaml!569 Michelson : Add proof for dep_parse_instr_eq | Reply to thread |
dhilst
is the original author |
| Add a merge-team reviewer |
dhilst
is the original author |
|
| Help add merge-team reviewers |
davdumas
jgonlabs
klakplok
MBourgoin
nguyencharles.nlabs
OanaLP
onurb
pirbo
raphael-proust
romain.nl
SamREye
vbotbol
is a dispatcher |
|
| 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 |
|
| Review or approve |
dhilst
is set as reviewer |
|
| Help add merge-team reviewers |
davdumas
jgonlabs
klakplok
MBourgoin
nguyencharles.nlabs
OanaLP
onurb
pirbo
raphael-proust
romain.nl
SamREye
vbotbol
is a dispatcher |
|
| nomadic-labs/coq-tezos-of-ocaml!528 Added proof for substr_l_eq | Reply to thread |
RektYuan
is the original author |
| Fix CI |
RektYuan
is the original author and triggered last pipeline |
|
| Add a merge-team reviewer |
RektYuan
is the original author |
|
| Help add merge-team reviewers |
davdumas
jgonlabs
klakplok
MBourgoin
nguyencharles.nlabs
OanaLP
onurb
pirbo
raphael-proust
romain.nl
SamREye
vbotbol
is a dispatcher |
|
| nomadic-labs/coq-tezos-of-ocaml#138 Translator simulations 50-59 michelson sprint-3 sprint-4 | Complete task |
kewersonhugo
is assigned |
| nomadic-labs/coq-tezos-of-ocaml#137 Translator simulations 40-49 michelson sprint-3 sprint-4 | Complete task |
deepmindster
is assigned |
| nomadic-labs/coq-tezos-of-ocaml#141 Translator simulations 80-89 michelson sprint-3 sprint-4 | Complete task |
dhilst
is assigned |
| nomadic-labs/coq-tezos-of-ocaml#98 Encodings in 🗂️ Indexable.v data-encoding sprint-4 | Complete task |
webmathew
is assigned |
| nomadic-labs/coq-tezos-of-ocaml#100 Encodings in ⚗️ Liquidity_baking_repr.v data-encoding sprint-4 | Complete task |
webmathew
is assigned |
| nomadic-labs/coq-tezos-of-ocaml#103 Encodings in 🎲 Sampler.v data-encoding | Complete task |
webmathew
is assigned |
| 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/coq-tezos-of-ocaml#71 Verify the non-iterable data stores storage | Solve issue |
clarus1
is assigned |
| nomadic-labs/coq-tezos-of-ocaml#139 Translator simulations 60-69 michelson sprint-3 sprint-4 | Solve issue |
deepmindster
is assigned |
| nomadic-labs/coq-tezos-of-ocaml#140 Translator simulations 70-79 michelson sprint-3 sprint-4 | Solve issue |
RektYuan
is assigned |
| nomadic-labs/coq-tezos-of-ocaml#154 Translate test_tx_rollup_l2_encoding.ml coq-of-ocaml tests | Solve issue |
TinoAlfie
is assigned |
| nomadic-labs/coq-tezos-of-ocaml#198 Tez: Verify test_coherent_mul_proof tests | Solve issue |
tudoroscoiu
is assigned |
| nomadic-labs/coq-tezos-of-ocaml#199 Tez: Verify test_coherent_div_proof tests | Solve issue |
tudoroscoiu
is assigned |
| nomadic-labs/coq-tezos-of-ocaml#101 Encodings in 🧑 Main.v data-encoding sprint-4 Blocked by nomadic-labs/coq-tezos-of-ocaml!560 | Unblock |
webmathew
is assigned |
| nomadic-labs/coq-tezos-of-ocaml#102 Encodings in 🖼️ Raw_context.v data-encoding sprint-4 Blocked by nomadic-labs/coq-tezos-of-ocaml!560 | Unblock |
webmathew
is assigned |
| nomadic-labs/coq-tezos-of-ocaml#127 Verify carbonated maps (3/3) carbonated maps sprint-3 sprint-4 Blocked by nomadic-labs/coq-tezos-of-ocaml!508 | Unblock |
emarzion
is assigned |
| nomadic-labs/coq-tezos-of-ocaml#135 Translator simulations 20-29 michelson sprint-3 sprint-4 Blocked by nomadic-labs/coq-tezos-of-ocaml!504 | Unblock |
kumar.shubham.off
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/coq-tezos-of-ocaml#64 Size function of Michocoq map returns the wrong size michelson | Solve issue |
kewersonhugo
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#42 ocaml 4.13 | Solve issue |
deepmindster
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#51 An invariant required for storage_functors.v | Solve issue |
webmathew
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#168 Use of conventions during the translation to verify exceptions and errors in the protocol | Solve issue |
dhilst
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!517 Draft: Skip list backpath | Close or reply to thread |
webmathew
is the thread author |
| Close or reply to thread |
webmathew
is the thread author |
|
| Close or reply to thread |
webmathew
is the thread author |
|
| Close or reply to thread |
webmathew
is the thread author |
|
| Close or reply to thread |
webmathew
is the thread author |
|
| UnWIP |
webmathew
is the original author |
|
| nomadic-labs/coq-tezos-of-ocaml!562 Draft: Michelson : Add proofs for dep_extract_lazy_storage_updates and dep_fold_lazy_storage_eq | Close or reply to thread |
dhilst
is the thread author |
| Close or reply to thread |
dhilst
is the thread author |
|
| Fix CI |
dhilst
is the original author and triggered last pipeline |
|
| UnWIP |
dhilst
is the original author |
|
| nomadic-labs/coq-tezos-of-ocaml!571 Draft: Add proof for dep_parse_contract_aux_eq and dep_parse_contract_for_script_eq | Close or reply to thread |
kewersonhugo
is the thread author |
| Reply to thread |
kewersonhugo
is the original author |
|
| Fix CI |
kewersonhugo
is the original author and triggered last pipeline |
|
| UnWIP |
kewersonhugo
is the original author |
|
| 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 |
| Close or reply to thread |
dhilst
is the thread author |
|
| Close or reply to thread |
webmathew
is the thread author |
|
| Reply to thread |
kumar.shubham.off
is the original author |
|
| Reply to thread |
kumar.shubham.off
is the original author |
|
| Fix CI |
kumar.shubham.off
is the original author |
|
| UnWIP |
kumar.shubham.off
is the original author |
|
| 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 |
| Close or reply to thread |
dhilst
is the thread author |
|
| Close or reply to thread |
deepmindster
is the thread author |
|
| Close or reply to thread |
deepmindster
is the thread author |
|
| Close or reply to thread |
dhilst
is the thread author |
|
| Fix CI |
deepmindster
is the original author and triggered last pipeline |
|
| UnWIP |
deepmindster
is the original author |
|
| nomadic-labs/coq-tezos-of-ocaml!250 Draft: -- not for comments yet -- | Fix CI |
deepmindster
is the original author and triggered last pipeline |
| UnWIP |
deepmindster
is the original author |
|
| nomadic-labs/coq-tezos-of-ocaml!326 Draft: Progress dep_step_eq | Fix CI |
emarzion
pushed recently and triggered last pipeline |
| UnWIP |
emarzion
pushed recently |
|
| 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/coq-tezos-of-ocaml!388 Draft: Arith code | Fix CI |
kewersonhugo
is the original author and triggered last pipeline |
| UnWIP |
kewersonhugo
is the original author |
|
| nomadic-labs/coq-tezos-of-ocaml!524 Draft: Simulation of parse_instr michelson | UnWIP |
clarus1
is the original author |
| nomadic-labs/coq-tezos-of-ocaml!570 Draft: Simulation : Add proof for dep_collect_storage_updates | UnWIP |
dhilst
is the original author |
Repositories
|
