search

verified-network-toolchain / petr4

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

Unify fresh name generators using Iris stdpp #430

Closed hackedy closed 1 year ago

hackedy commented 1 year ago

This pull request turns several fresh name generators into one fresh name generator that relies on an efficient implementation of finite maps and name-freshening found in the Iris stdpp library.

hackedy commented 1 year ago

I can't reproduce the CI build failure locally....

hackedy commented 1 year ago

It builds on my machine but some tests fail because the name generator is a little stricter than the old one about observing the same name twice. Working on it

hackedy commented 1 year ago

Whatever is going on in CI seems like CI flakiness. I couldn't reproduce it in a clean local Ubuntu VM and the Mac CI passed.

hackedy commented 1 year ago

I think the problem here is that Iris modules are named in lower case (so, stdpp.stringmap not stdpp.Stringmap) and this is no problem on a case insensitive file system like my laptop. But on an actual case sensitive filesystem it breaks the dune extracted_modules check somehow.

hackedy commented 1 year ago

Fixed CI, ready for review!

rudynicolop commented 1 year ago

Should this be merged before or after #434?

hackedy commented 1 year ago

Should this be merged before or after #434?

Merge #434 first and I can adjust this PR to deal with any conflicts.

hackedy commented 1 year ago

Turns out the PRs are totally independent because P4cub doesn't need fresh name generation anywhere (due to de Bruijn) 👍