spitters
commented
7 months ago There is now better support for primitive types, like the integers, in metacoq/certicoq. We should probably be using it in rust extraction too. @womeier has also been looking at it recently
On Tue, Mar 19, 2024 at 6:18 PM Jubilee @.***> wrote:
The Rust compiler is unlikely to successfully compile anything that requires explosively recursive expressions. Even after rust-lang/rust#122717 https://github.com/rust-lang/rust/pull/122717 for example, it will still have to actually finish trait resolving, borrow checking, and codegen. Also, it will be obviously slow. Use of an intermediate encoding that is amenable to applying a rewrite rule to eliminate the redexes, and actually applying such a rule during extraction, would be preferable. That way you don't have to assume that rustc will put up with being force-fed an infinite amount of abstract nonsense.
The more general cases regarding inefficient implementation work are already discussed by other authors such as Jansen, Koopman, and Plasmeijer, i.e. https://repository.ubn.ru.nl/bitstream/handle/2066/151174/151174.pdf?sequence=1&isAllowed=y
— Reply to this email directly, view it on GitHub https://github.com/AU-COBRA/coq-rust-extraction/issues/17, or unsubscribe https://github.com/notifications/unsubscribe-auth/AABTNTVCOOEFVK76RE73RETYZBXOLAVCNFSM6AAAAABE572EYSVHI2DSMVQWIX3LMV43ASLTON2WKOZSGE4TKNJUGI2DGMY . You are receiving this because you are subscribed to this thread.Message ID: @.***>
workingjubilee
4ever2
womeier
The Rust compiler is unlikely to successfully compile anything that requires explosively recursive expressions. Even after https://github.com/rust-lang/rust/pull/122717 for example, it will still have to actually finish trait resolving, borrow checking, and codegen. Also, it will be obviously slow. Use of an intermediate encoding that is amenable to applying a rewrite rule to eliminate the redexes, and actually applying such a rule during extraction, would be preferable. That way you don't have to assume that rustc will put up with being force-fed an infinite amount of abstract nonsense.
The more general cases regarding inefficient implementation work are already discussed by other authors such as Jansen, Koopman, and Plasmeijer, i.e. https://repository.ubn.ru.nl/bitstream/handle/2066/151174/151174.pdf?sequence=1&isAllowed=y