search

verified-network-toolchain / petr4

Petr4: Formal Semantics for P4
Apache License 2.0
75 stars 21 forks source link

Make the main branch compatible with Coq 8.16.1 #445

Closed txyyss closed 1 year ago

txyyss commented 1 year ago

Some automation does not work for Coq 8.16. I fixed one but still have to leave some manual proof. If any of you have time, we can have a Zoom meeting to discuss how to improve the current fix.

I only test the code on Coq 8.16.1. It may break on Coq 8.15.

hackedy commented 1 year ago

Looks like CI is failing because it runs it on Coq 8.15. Should we just require 8.16 in the dune-project file? (The opam file is generated by Dune from the dependencies in the dune-project file so it shouldn't be edited manually)

hackedy commented 1 year ago

Yeah CI is using 8.15.2 https://github.com/verified-network-toolchain/petr4/actions/runs/5466619661/jobs/9951808416#step:5:69

txyyss commented 1 year ago

Yeah CI is using 8.15.2 https://github.com/verified-network-toolchain/petr4/actions/runs/5466619661/jobs/9951808416#step:5:69

Should I configure the CI of this branch to make it work first? or should I tweak the proof script to make it compatible for both 8.15 and 8.16.

hackedy commented 1 year ago

Should I configure the CI of this branch to make it work first? or should I tweak the proof script to make it compatible for both 8.15 and 8.16.

Proof script tweaks would be less disruptive but if it ends up being too complicated to fix an upgrade would be fine with me.

txyyss commented 1 year ago

Should I configure the CI of this branch to make it work first? or should I tweak the proof script to make it compatible for both 8.15 and 8.16.

Proof script tweaks would be less disruptive but if it ends up being too complicated to fix an upgrade would be fine with me.

Some of my upgrade fix is ad hoc when automatic tactics failed. For example, the CI failed with Error: No such goal. because on 8.16 the tactic would leave an unsolved goal while on 8.15 it would not. Since I'm not familiar with existing proof I can not figure out which trial failed on 8.16. So if you have time this week or future, I would like to have a Zoom meeting with you to discuss how to fix it in a better way, without breaking the automation. Thank you very much.

hackedy commented 1 year ago

Hi, I think I patched the proofs up. Sorry for the late reply but it was a quick fix.