Skip to content

Commit

Permalink
Chore: No formatting of the generated Rust file but better indent (#6069
Browse files Browse the repository at this point in the history
)

### What was changed?
The Rust formatter is usually _crashing_ on generated files on big
codebases.
Since it's hard to pinpoint the cause of the crashing, instead, I change
the default generation indentation to 4 spaces like Rust and deactivate
formatting on generated files.

### How has this been tested?
Existing tests should pass

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
  • Loading branch information
MikaelMayer authored Jan 23, 2025
1 parent bf9cf16 commit 6faf1c5
Show file tree
Hide file tree
Showing 6 changed files with 4,004 additions and 4,001 deletions.
2 changes: 1 addition & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -114,7 +114,7 @@ update-go-module:
update-runtime-dafny:
(cd "${DIR}"; cd Source/DafnyRuntime/DafnyRuntimeDafny; make update-go)

pr-nogeneration: format-dfy format update-runtime-dafny update-cs-module update-rs-module update-go-module update-rs-module
pr-nogeneration: format-dfy format update-runtime-dafny update-cs-module update-rs-module update-go-module

update-standard-libraries:
(cd "${DIR}"; cd Source/DafnyStandardLibraries; make update-binary)
Expand Down
4 changes: 2 additions & 2 deletions Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-rast.dfy
Original file line number Diff line number Diff line change
Expand Up @@ -12,8 +12,8 @@ module RAST
// Past that, we use Dafny system tuples (see https://www.reddit.com/r/rust/comments/11gvkda/why_rust_std_only_provides_trait_implementation/)
const MAX_TUPLE_SIZE := 12

// Default Indentation
const IND := " "
// Default Rust-like indentation
const IND := " "

datatype RASTTopDownVisitor<!T(!new)> =
RASTTopDownVisitor(
Expand Down
1 change: 1 addition & 0 deletions Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy
Original file line number Diff line number Diff line change
Expand Up @@ -4068,6 +4068,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
{
s := "#![allow(warnings, unconditional_panic)]\n";
s := s + "#![allow(nonstandard_style)]\n";
s := s + "#![cfg_attr(any(), rustfmt::skip)]\n"; // Because Rustfmt crashes on some generated files

var externUseDecls := [];

Expand Down
1 change: 1 addition & 0 deletions Source/DafnyCore/GeneratedFromDafny/DCOMP.cs
Original file line number Diff line number Diff line change
Expand Up @@ -6764,6 +6764,7 @@ public RAST._IExpr Error(Dafny.ISequence<Dafny.Rune> message, RAST._IExpr defaul
Dafny.ISequence<Dafny.Rune> s = Dafny.Sequence<Dafny.Rune>.Empty;
s = Dafny.Sequence<Dafny.Rune>.UnicodeFromString("#![allow(warnings, unconditional_panic)]\n");
s = Dafny.Sequence<Dafny.Rune>.Concat(s, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("#![allow(nonstandard_style)]\n"));
s = Dafny.Sequence<Dafny.Rune>.Concat(s, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("#![cfg_attr(any(), rustfmt::skip)]\n"));
Dafny.ISequence<RAST._IModDecl> _0_externUseDecls;
_0_externUseDecls = Dafny.Sequence<RAST._IModDecl>.FromElements();
BigInteger _hi0 = new BigInteger((externalFiles).Count);
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyCore/GeneratedFromDafny/RAST.cs
Original file line number Diff line number Diff line change
Expand Up @@ -174,7 +174,7 @@ public static RAST._IExpr IntoUsize(RAST._IExpr underlying) {
return (((RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyUsize"))).FSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("into_usize"))).Apply1(underlying);
}
public static Dafny.ISequence<Dafny.Rune> IND { get {
return Dafny.Sequence<Dafny.Rune>.UnicodeFromString(" ");
return Dafny.Sequence<Dafny.Rune>.UnicodeFromString(" ");
} }
public static RAST._IType SelfOwned { get {
return (RAST.Path.create_Self()).AsType();
Expand Down
Loading

0 comments on commit 6faf1c5

Please sign in to comment.