New IDE support - #109

Merged

Aurel300 merged 123 commits into

Aurel300:rewrite-2023from

zgrannan:zgrannan/ide

Nov 3, 2025

Commits on Jun 3, 2024

Fix domain function name garbling when running over prusti-server
trktby
committed
30beba6

Commits on Jun 8, 2024

Use new VerificationResult type
trktby
committed
ec4035e

Commits on Jun 12, 2024

Change prusti-server workflow
trktby
committed
4e6cc8a

Commits on Jun 13, 2024

Port `show_ide_info` and `skip_verification` flags
trktby
committed
0849d35
Port `verify_only_defpath` and `report_viper_messages` flags
trktby
committed
5270e09

Commits on Jun 14, 2024

Add support for block level messaging and bump version
trktby
committed
39bfc55

Commits on Jun 18, 2024

Attempt to fix the only defpath flag and fix not emitting fake error
trktby
committed
99c3b2c
Port call finder
trktby
committed
e607cc0
Attempt porting QUERY_METHOD_SIGNATURE flag
trktby
committed
d472c60

Commits on Jul 5, 2024

Improve contract span emission
trktby
committed
1443c24

Commits on Jul 12, 2024

Accept defpaths argument as a single string
trktby
committed
cd45907
WIP: Restructure how verification requests are handled
trktby
committed
9f58eef
Optimize selective encoding for the non-selective case, config bug fix
trktby
committed
1de40ff

Commits on Jul 15, 2024

Use cfg_if instead of if(cfg!()) (#49)

zgrannan
authored and
trktby
committed
aaecb18
Impure Generics (#45)

zgrannan
authored and
trktby
committed
bc26f7b
Support cycles in encoders (#47)

Aurel300
authored and
trktby
committed
ca5edb3
VIR span manager, backtranslate postcondition errors

Aurel300
authored and
trktby
committed
f8527cc
add spans to statements, backtranslate precondition errors

Aurel300
authored and
trktby
committed
c513772
fix VIR translation errors

Aurel300
authored and
trktby
committed
e977267
cast tuple components in pure contexts

Aurel300
authored and
trktby
committed
0408617
update Viper toolchain, to avoid error filtering (see Silicon#735)

Aurel300
authored and
trktby
committed
9a99465
small generic fixes

Aurel300
authored and
trktby
committed
f3cf4ef
handle assertion failures, add precondition precision

Aurel300
authored and
trktby
committed
f53725a
Post-rebase fixes
trktby
committed
846c447

Commits on Jul 16, 2024

Port quantifier features skelleton from PR
trktby
committed
14025ce

Commits on Jul 18, 2024

Fix typo
trktby
committed
70b9855
Fix viper program passing and factor out cache
trktby
committed
d195424

Commits on Jul 19, 2024

Commits on Jul 20, 2024

Add back stopwatch calls
trktby
committed
1b64b36

Commits on Jul 22, 2024

Translate and emit quantifier messages
trktby
committed
a9e5021

Commits on Jul 25, 2024

Parse pos_id as usize instead of u64 in quant messages
trktby
committed
b5722f3
More server refactoring
trktby
committed
2f8c64f

Commits on Aug 1, 2024

Fix flag to use actual vectors
trktby
committed
f06740f
Move IDE related functionality to an own top-level crate
trktby
committed
9b2bf78
Move contract span collection and fix selective encoding
trktby
committed
47591c4

Commits on Aug 2, 2024

Emit entire procedure span rather than just signature in CompilerInfo
trktby
committed
ee1747c
Add viper method name backtranslation
trktby
committed
174aef5
Revert contract spans having multiple call spans
trktby
committed
b8c37ed

Commits on Aug 8, 2024

Report results per method, backtranslate block labels
trktby
committed
1ebf520

Commits on Aug 12, 2024

Merge branch 'assistant-features/request-processing-restructure' into rewrite-2023-assistant-features
trktby
committed
3e78249

Commits on Aug 15, 2024

Commits on Aug 20, 2024

Revert "small generic fixes"
trktby
committed
b708b7c
Add type parameters to pure make_generic method for consistency

erdmannc
authored and
trktby
committed
fd951ed

Commits on Aug 21, 2024

improve support for closures/quantifiers

Aurel300
authored and
trktby
committed
19de80e
Filter some block statements for range map
trktby
committed
da102cc

Commits on Aug 29, 2024

Adapt for passing through `BlockFailureMessage`s
trktby
committed
e5a323b

Commits on Aug 30, 2024

Remove most `program_name` variables from calls
trktby
committed
ef98dc6

Commits on Sep 2, 2024

Do some simplifying and add comments
trktby
committed
a614769

Commits on Oct 4, 2025

Merge
zgrannan
committed
ef1bee7

Commits on Oct 5, 2025

WIP
zgrannan
committed
16e8051

Commits on Oct 6, 2025

WIP
zgrannan
committed
8bd3586
Compiles
zgrannan
committed
8162db1
WIP
zgrannan
committed
cbbafd4
merge
zgrannan
committed
4706787
WIP
zgrannan
committed
5628d69
remove unused
zgrannan
committed
f28d75c
remove unused
zgrannan
committed
26ee35d
remove unused
zgrannan
committed
8baee7b
remove unused
zgrannan
committed
f17e161
fmt
zgrannan
committed
a518504

Commits on Oct 7, 2025

WIP
zgrannan
committed
3a1f5af
Fix compiler warnings
zgrannan
committed
39870ff
clippy
zgrannan
committed
775869d
small cleanup
zgrannan
committed
fa7e054
fixes
zgrannan
committed
66b0622
deploy artifact
zgrannan
committed
ac5d2c4
Update deploy version
zgrannan
committed
20ca058
recursive submodules
zgrannan
committed
5125675
WIP
zgrannan
committed
fc1d11a
fix arch
zgrannan
committed
5075dee
dont pass in arch
zgrannan
committed
57f8aca
fixes
zgrannan
committed
409ae19
try recent java version
zgrannan
committed
f907a17
update versions
zgrannan
committed
4e38dd3
CI updates
zgrannan
committed
8c63a51
Update
zgrannan
committed
f8f3523
WIP
zgrannan
committed
5cd069a

Commits on Oct 8, 2025

Update Rust toolchain
zgrannan
committed
2ecfe01
Update PCG and rust toolchain
zgrannan
committed
65a4099
Update PCG
zgrannan
committed
5436ca5
fix prusti launch tests
zgrannan
committed
636179b
Update
zgrannan
committed
c4f93f4
try fix windows CI
zgrannan
committed
760064e
Fix tests?
zgrannan
committed
a9c7dfd

Commits on Oct 9, 2025

remove invalid program test
zgrannan
committed
635f27d
try fix windows CI
zgrannan
committed
04a8e96
Fix doctest
zgrannan
committed
68e8f4b

Commits on Oct 10, 2025

Update PCG for windows CI fixes
zgrannan
committed
c14657e
Windows CI fix
zgrannan
committed
16f59bf
Remove ubuntu 20.04
zgrannan
committed
d1ded62
Remove ubuntu 20.04
zgrannan
committed
c575a6a

Commits on Oct 13, 2025

update submodule
zgrannan
committed
42bab3e
Revert "update submodule"
zgrannan
committed
363ade6
windows aarch64
zgrannan
committed
2c294ed
switch to vendored deps
zgrannan
committed
90556e0

Commits on Oct 14, 2025

Update PCG
zgrannan
committed
38e2be2

Commits on Oct 15, 2025

update CI, fmt
zgrannan
committed
4b57540
15 -> 16
zgrannan
committed
ba64dea
fix clippy issues
zgrannan
committed
f59cebd
try fix
zgrannan
committed
7ced18c

Commits on Oct 16, 2025

WIP
zgrannan
committed
4b07baa

Commits on Oct 23, 2025

WIP
zgrannan
committed
650e905
better error
zgrannan
committed
570c83b
remove fakeerror
zgrannan
committed
5fc1fc0
Revert "remove fakeerror"
zgrannan
committed
003ecbd
Add more to loader path
zgrannan
committed
46252bb
refactor
zgrannan
committed
df8477d
remove rustc_hash dependency
zgrannan
committed
e66e1cf
WIP
zgrannan
committed
13bfbd5
Revert "WIP"
zgrannan
committed
ae9740b

Commits on Oct 24, 2025

Fix tests (#105)

Aurel300
authored and
zgrannan
committed
557cdcd
clippy, cargo fmt
zgrannan
committed
3e982cb
Fix tests
zgrannan
committed
e991228
Only build artifacts on master
zgrannan
committed
c5c5f49
Try new workflow
zgrannan
committed
eff727b
fix a typo
zgrannan
committed
016b919

Commits on Oct 27, 2025

remove stuff specific to my branch
zgrannan
committed
745906b