Gamedev Mastodon

0 posts0 participants0 posts today

Jan :rust: :ferris:Hm...I'm running into a timeout with <a href="https://floss.social/tags/Creusot" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Creusot</a> when trying to verify a simple `add` operation on a HashMap newtype 🤔 <a href="https://github.com/creusot-rs/creusot/discussions/1477" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://github.com/creusot-rs/creusot/discussions/1477</a>Does anyone have any idea what's going on here?Disclaimer: I'm totally new to creusot and <a href="https://floss.social/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FormalVerification</a>, so please be gentle with me.😊 Boosts very much appreciated. :boost_love: Thank you! ❤️ <a href="https://floss.social/tags/IDontKnowWhatIamDoing" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IDontKnowWhatIamDoing</a> <a href="https://floss.social/tags/Help" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Help</a> <a href="https://floss.social/tags/FediHelp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FediHelp</a> <a href="https://floss.social/tags/FollowerPower" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FollowerPower</a> <a href="https://floss.social/tags/Rust" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Rust</a> <a href="https://floss.social/tags/RustLang" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#RustLang</a> <a href="https://floss.social/tags/Proof" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Proof</a> <a href="https://floss.social/tags/Timeout" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Timeout</a>

Jan :rust: :ferris:creuSAT - A formally verified <a href="https://floss.social/tags/SAT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#SAT</a> solver written in <a href="https://floss.social/tags/Rust" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Rust</a> and verified with <a href="https://floss.social/tags/Creusot" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Creusot</a>.<a href="https://github.com/sarsko/CreuSAT" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://github.com/sarsko/CreuSAT</a>Mindblowing! 🤯 <a href="https://floss.social/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FormalVerification</a> <a href="https://floss.social/tags/RustLang" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#RustLang</a>

Jan :rust: :ferris:Nice, I think I've found a (for me) suitable workaround for the above problem 👆 :awesome: => <a href="https://github.com/creusot-rs/creusot/issues/1337#issuecomment-2821430387" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://github.com/creusot-rs/creusot/issues/1337#issuecomment-2821430387</a>The "trick" is to use conditional compilation with `cfg` and `cfg_attr`, so we don't derive or use `Debug` when in context of Creusot.See the above linked comment on how to do this exactly.More on `cfg`, `cfg_attr` and conditional compilation in the <a href="https://floss.social/tags/Rust" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Rust</a> reference:<a href="https://doc.rust-lang.org/reference/conditional-compilation.html" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://doc.rust-lang.org/reference/conditional-compilation.html</a><a href="https://floss.social/tags/RustLang" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#RustLang</a> <a href="https://floss.social/tags/Creusot" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Creusot</a> <a href="https://floss.social/tags/Bug" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Bug</a> <a href="https://floss.social/tags/Workaround" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Workaround</a>

Jan :rust: :ferris:Seems like I'm living on the bleeding edge of formal verification in <a href="https://floss.social/tags/Rust" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Rust</a>!Ouch! 😢 ⚔️ 🩸 => <a href="https://github.com/creusot-rs/creusot/issues/1337#issuecomment-2819513924" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://github.com/creusot-rs/creusot/issues/1337#issuecomment-2819513924</a><a href="https://floss.social/tags/Creusot" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Creusot</a> <a href="https://floss.social/tags/RustLang" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#RustLang</a> <a href="https://floss.social/tags/ICE" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ICE</a> <a href="https://floss.social/tags/Bug" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Bug</a>

Athenenoctua<a href="https://mastodon.gougere.fr/tags/PhotoJanuary2025" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#PhotoJanuary2025</a> Jour 13 : artificielNon vous n'avez pas été drogués à l'insu de votre plein gré : cette allée du parc de la Verrerie au <a href="https://mastodon.gougere.fr/tags/creusot" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#creusot</a> arbore une <a href="https://mastodon.gougere.fr/tags/couleur" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#couleur</a> tout ce qu'il y a de plus artificiel dans le cadre de jeux d'été 🪅 Ou comment voir la vie en rose alors qu'on est en train de vider l'appartement maternel 😬Septembre 2023<a href="https://mastodon.gougere.fr/tags/photography" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#photography</a> <a href="https://mastodon.gougere.fr/tags/saonetloire" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#saonetloire</a>

Recent searches

Search options

Administered by:

Server stats:

#Creusot