I am trying to generate a unified dataset of the modules in Everest, where every module name occurs exactly once (i.e., where you can put all the source files in a single directory). However, there are several name clashes that are in the way.
The biggest one is probably Mem.fst. This file occurs both in EverQuic and in miTLS, and with different contents. This clash prevents us from including most of miTLS. (There's also QUIC.fst in these two projects with the same issue.)
miTLS has many modules twice, in both a Model and a Karamel variant. We have tentatively decided to favor the Model directory because it's the one with the proofs.
EverParse has both a buffer and an extern implementation.
There's lots of modules with very generic, unqualified names. Such as for example Test.fst in HACL, which causes shadowing together with FStar.Test.fst. Most of the unqualified module names are in miTLS and EverParse (and some more in EverQuic, Karamel, HACL).
Some prefixes are used in multiple projects, e.g. HACL* has Lib.Buffer.fst while merkle-tree has Lib.RawBuffer.fst.
Skipping duplicate module /home/gebner/everest/everparse/src/3d/prelude/extern/EverParse3d.Actions.BackendFlagValue.fsti.checked in favor of ('/home/gebner/everest/everparse/src/3d/prelude/buffer/EverParse3d.Actions.BackendFlagValue.fsti.checked', '/home/gebner/everest/everparse/src/3d/prelude/buffer/EverParse3d.Actions.BackendFlagValue.fsti')
Skipping duplicate module /home/gebner/everest/everparse/src/3d/prelude/extern/EverParse3d.Actions.BackendFlagValue.fst.checked in favor of ('/home/gebner/everest/everparse/src/3d/prelude/buffer/EverParse3d.Actions.BackendFlagValue.fst.checked', '/home/gebner/everest/everparse/src/3d/prelude/buffer/EverParse3d.Actions.BackendFlagValue.fst')
Skipping duplicate module /home/gebner/everest/everparse/src/3d/prelude/extern/EverParse3d.InputStream.All.fst.checked in favor of ('/home/gebner/everest/everparse/src/3d/prelude/buffer/EverParse3d.InputStream.All.fst.checked', '/home/gebner/everest/everparse/src/3d/prelude/buffer/EverParse3d.InputStream.All.fst')
Skipping /home/gebner/everest/everparse/src/3d/prelude/extern/EverParse3d.Actions.All.fst.checked because of unavailable dependency everparse3d.inputstream.all
Skipping duplicate module /home/gebner/everest/everparse/src/3d/prelude/extern/EverParse3d.Actions.BackendFlag.fst.checked in favor of ('/home/gebner/everest/everparse/src/3d/prelude/buffer/EverParse3d.Actions.BackendFlag.fst.checked', '/home/gebner/everest/everparse/src/3d/prelude/buffer/EverParse3d.Actions.BackendFlag.fst')
Skipping /home/gebner/everest/hacl-star/obj/Test.fst.checked because name causes lots of shadowing
Skipping /home/gebner/everest/hacl-star/obj/Test.fsti.checked because name causes lots of shadowing
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.NamedGroup.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.TicketContents12_master_secret.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.TicketContents13.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Old.Handshake.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/LHAEPlain.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.NamedGroupList.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.TicketContents12_master_secret.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Ticket.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/HandshakeLog.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/TLSInfoFlags.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Record.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Negotiation.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Test.Main.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.AlertLevel.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/KDF.Rekey.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Old.HMAC.UFCMA.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/PKI.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Hashing.CRF.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Connection.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/CommonDH.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.CompressionMethod.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.ECCurveType.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/IV.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Idx.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/DHGroup.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.Boolean.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.HKDF.HkdfLabel_label.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/TLSInfo.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/HandshakeMessages.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.TicketContents.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.CompressionMethod.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/HandshakeMessages.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.NamedGroup.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.AlertDescription.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.CipherSuite.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.SignatureSchemeList.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Cert.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/StatefulPlain.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/FFI.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/TLSError.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.ECCurveType.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/KDF.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Old.KeySchedule.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Cert.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/TLS.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.TicketVersion.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Extensions.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Old.Epochs.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.SignatureSchemeList.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.TicketContents13_rms.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.SignatureScheme.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/HKDF.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Extensions.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/StAE.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.TicketContents12_master_secret.Low.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.Alert.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.TicketContents13_nonce.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Test.Handshake.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Hashing.CRF.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Record.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/DHGroup.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.AlertDescription.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.TicketContents12.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Crypto.Plain.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/RSAKey.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/AEADProvider.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Range.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Test.CommonDH.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Crypto.Indexing.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Transport.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/StreamAE.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/StatefulLHAE.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Crypto.Symmetric.Bytes.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.Boolean.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Pkg.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.ProtocolVersion.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/DataStream.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/HandshakeLog.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.TicketContents12.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Hashing.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Model.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Random.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Test.TLSConstants.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.TicketContents.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/CommonDH.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Alert.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/BufferBytes.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Format.KeyShareEntry.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.Alert.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parse.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.CipherSuite.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/LowParseWrappers.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.HKDF.HkdfLabel.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.AlertLevel.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Format.KeyShareEntry.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Flag.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Old.KeySchedule.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/TLSPRF.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/TLSConstants.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.TicketContents12_master_secret.Low.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Content.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/StreamPlain.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Nonce.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.HKDF.HkdfLabel_context.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Old.HMAC.UFCMA.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Hashing.Spec.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/QUIC.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Mem.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/TLS.Curve25519.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/TLSConstants.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.Ticket.Low.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.SignatureScheme.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Format.UncompressedPointRepresentation.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.TicketContents13_custom_data.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/ECGroup.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.TicketContents13_custom_data.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/EverCrypt.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/HMAC.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/AEAD_GCM.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.HKDF.HkdfLabel_context.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/CipherSuite.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.TicketContents13_nonce.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.TicketVersion.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Test.AEAD.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Test.StAE.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/ECGroup.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Old.Epochs.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Pkg.Tree.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.NamedGroupList.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Buffer.Utils.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/StreamDeltas.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/PSK.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Hashing.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/EverCrypt.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.HKDF.HkdfLabel_label.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.ProtocolVersion.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/AEADProvider.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Test.BufferBytes.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/List.Helpers.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Format.UncompressedPointRepresentation.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/CipherSuite.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Nonce.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.TicketContents13_rms.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Old.Handshake.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.TicketContents13.fsti.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Crypto.Plain.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Parsers.HKDF.HkdfLabel.fst.checked because module name clashes with the Model variant
Skipping duplicate module /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Mem.fst.checked in favor of ('/home/gebner/everest/everquic-crypto/obj/Mem.fst.checked', '/home/gebner/everest/everquic-crypto/src/Mem.fst')
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Parse.fst.checked because of unavailable dependency mem
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/TLSConstants.fsti.checked because of unavailable dependency parse
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Test.TLSConstants.fst.checked because of unavailable dependency tlsconstants
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Test.Main.fst.checked because of unavailable dependency test.tlsconstants
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/PMS.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/TLSInfoFlags.fst.checked because of unavailable dependency tlsconstants
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/TLSInfo.fst.checked because of unavailable dependency tlsinfoflags
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Old.Handshake.fsti.checked because of unavailable dependency tlsinfo
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Karamel/Flags.fst.checked because module name clashes with the Model variant
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Pkg.fst.checked because of unavailable dependency mem
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/AEAD.Pkg.fsti.checked because of unavailable dependency pkg
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Negotiation.fst.checked because of unavailable dependency tlsinfo
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Random.fst.checked because of unavailable dependency mem
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/IV.fst.checked because of unavailable dependency random
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Ticket.fst.checked because of unavailable dependency tlsinfo
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/LHAEPlain.fst.checked because of unavailable dependency tlsinfo
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Old.HMAC.UFCMA.fsti.checked because of unavailable dependency tlsinfo
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Old.HMAC.UFCMA.fst.checked because of unavailable dependency interface
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/HandshakeLog.fsti.checked because of unavailable dependency tlsinfo
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Transport.fst.checked because of unavailable dependency mem
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Record.fsti.checked because of unavailable dependency transport
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Connection.fst.checked because of unavailable dependency transport
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Hashing.CRF.fsti.checked because of unavailable dependency mem
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Hashing.CRF.fst.checked because of unavailable dependency interface
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/PKI.fsti.checked because of unavailable dependency tlsconstants
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/CommonDH.fsti.checked because of unavailable dependency parse
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/CommonDH.fst.checked because of unavailable dependency interface
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Idx.fst.checked because of unavailable dependency tlsinfo
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/DHGroup.fst.checked because of unavailable dependency parse
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/HandshakeMessages.fsti.checked because of unavailable dependency tlsinfo
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/KDF.Rekey.fst.checked because of unavailable dependency random
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Cert.fsti.checked because of unavailable dependency tlsconstants
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/TLSPRF.fst.checked because of unavailable dependency tlsinfo
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Old.KeySchedule.fsti.checked because of unavailable dependency tlsprf
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/TLS.fst.checked because of unavailable dependency transport
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/HandshakeMessages.fst.checked because of unavailable dependency interface
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/StatefulPlain.fst.checked because of unavailable dependency tlsinfo
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Cert.fst.checked because of unavailable dependency interface
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Old.Epochs.fsti.checked because of unavailable dependency tlsinfo
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/FFI.fst.checked because of unavailable dependency transport
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/KDF.fst.checked because of unavailable dependency tlsinfo
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Extensions.fsti.checked because of unavailable dependency tlsconstants
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Extensions.fst.checked because of unavailable dependency interface
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Crypto.Indexing.fst.checked because of unavailable dependency tlsinfo
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Flag.fst.checked because of unavailable dependency crypto.indexing
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Crypto.Plain.fsti.checked because of unavailable dependency flag
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/RSAKey.fst.checked because of unavailable dependency tlsconstants
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Token.UF1CMA.fsti.checked because of unavailable dependency pkg
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Token.UF1CMA.fst.checked because of unavailable dependency interface
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/HKDF.fst.checked because of unavailable dependency mem
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Record.fst.checked because of unavailable dependency interface
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/StAE.fst.checked because of unavailable dependency tlsinfo
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Test.Handshake.fst.checked because of unavailable dependency tlsinfo
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/AEAD.Pkg.fst.checked because of unavailable dependency interface
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/StatefulLHAE.fst.checked because of unavailable dependency tlsinfo
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Range.fst.checked because of unavailable dependency tlsinfo
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/AEADProvider.fsti.checked because of unavailable dependency tlsinfo
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/StreamAE.fst.checked because of unavailable dependency tlsinfo
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/DataStream.fst.checked because of unavailable dependency tlsinfo
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Test.CommonDH.fst.checked because of unavailable dependency tlsconstants
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Model.fst.checked because of unavailable dependency mem
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/AEAD.fsti.checked because of unavailable dependency pkg
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/HandshakeLog.fst.checked because of unavailable dependency interface
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Hashing.fsti.checked because of unavailable dependency mem
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Alert.fst.checked because of unavailable dependency tlsinfo
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/TLSConstants.fst.checked because of unavailable dependency interface
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/LowParseWrappers.fst.checked because of unavailable dependency parse
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Old.KeySchedule.fst.checked because of unavailable dependency interface
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Content.fst.checked because of unavailable dependency tlsinfo
Skipping duplicate module /home/gebner/everest/mitls-fstar/src/tls/cache/Model/QUIC.fst.checked in favor of ('/home/gebner/everest/everquic-crypto/obj/QUIC.fst.checked', '/home/gebner/everest/everquic-crypto/src/QUIC.fst')
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/StreamPlain.fst.checked because of unavailable dependency tlsinfo
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Nonce.fsti.checked because of unavailable dependency tlsconstants
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/AEAD_GCM.fst.checked because of unavailable dependency tlsinfo
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/TLS.Curve25519.fst.checked because of unavailable dependency random
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/HMAC.fst.checked because of unavailable dependency mem
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/ECGroup.fsti.checked because of unavailable dependency tls.curve25519
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/ECGroup.fst.checked because of unavailable dependency interface
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/CipherSuite.fsti.checked because of unavailable dependency parse
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/CipherSuite.fst.checked because of unavailable dependency interface
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/StreamDeltas.fst.checked because of unavailable dependency tlsinfo
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Old.Epochs.fst.checked because of unavailable dependency interface
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Test.AEAD.fst.checked because of unavailable dependency tlsinfo
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Test.StAE.fst.checked because of unavailable dependency tlsinfo
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/HMAC.UFCMA.fst.checked because of unavailable dependency random
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Nonce.fst.checked because of unavailable dependency interface
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Hashing.fst.checked because of unavailable dependency interface
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Pkg.Tree.fst.checked because of unavailable dependency pkg
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/PSK.fst.checked because of unavailable dependency tlsconstants
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/AEADProvider.fst.checked because of unavailable dependency interface
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Crypto.Plain.fst.checked because of unavailable dependency interface
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/PMS.fst.checked because of unavailable dependency tlsconstants
Skipping /home/gebner/everest/mitls-fstar/src/tls/cache/Model/Old.Handshake.fst.checked because of unavailable dependency interface
I am trying to generate a unified dataset of the modules in Everest, where every module name occurs exactly once (i.e., where you can put all the source files in a single directory). However, there are several name clashes that are in the way.
Mem.fst. This file occurs both in EverQuic and in miTLS, and with different contents. This clash prevents us from including most of miTLS. (There's alsoQUIC.fstin these two projects with the same issue.)Test.fstin HACL, which causes shadowing together withFStar.Test.fst. Most of the unqualified module names are in miTLS and EverParse (and some more in EverQuic, Karamel, HACL).Lib.Buffer.fstwhile merkle-tree hasLib.RawBuffer.fst.