Add Agda certifier integration with source location tracking#7660
Add Agda certifier integration with source location tracking#7660
Conversation
SeungheonOh
left a comment
SeungheonOh
left a comment
There was a problem hiding this comment.
Left some comments, mainly over the compiler part. Second pair of eyes on certifier part would be nice since I'm not too familiar with that area
| @@ -6,4 +6,4 @@ Trace: | |||
| -> func (test/CallTrace/Spec.hs:79:1-79:4) | |||
There was a problem hiding this comment.
All test golden in test/CallTrace/* needs to be reverted. The call srcspan gets erased when we build from compilation cache.
Also, I think this can be fixed now. made an issue #7722
| consume _ = err | ||
| in | ||
| consume li >>= traverse (compileExpr Nothing) | ||
| consume li >>= traverse (compileExpr) |
There was a problem hiding this comment.
this didn't get caught by hlint? I'm surprised
| , ccCurrentLoc :: Maybe GHC.RealSrcSpan | ||
| , ccPackageName :: String | ||
| , ccModuleName :: String | ||
| , ccSourceLoc :: Maybe GHC.RealSrcSpan |
There was a problem hiding this comment.
what's for ccSourceLoc and what's for ccCurrentLoc?
I see ccSourceLoc is only used for verifier related stuff; can we not only have ccCurrentLoc and use that for verifier stuff?
| other -> other | ||
| {-| Strip a single @anchor@ application (and any surrounding ticks), | ||
| returning the decoded source span if present. -} | ||
| stripAnchors :: GHC.Name -> GHC.CoreExpr -> (Maybe GHC.RealSrcSpan, GHC.CoreExpr) |
There was a problem hiding this comment.
Maybe it's better to have separate getAnchorSrcSpan function instead of adding it to stripAnchors; or, give it some better name.
ana-pantilie
left a comment
ana-pantilie
left a comment
There was a problem hiding this comment.
The certifier changes are awesome, thanks @zeme-wana! The only issue I have with this PR is, as @SeungheonOh pointed out:
All test golden in test/CallTrace/* needs to be reverted. The call srcspan gets erased when we build from compilation cache.
3 participants
CompileContext (ccCurrentLoc) instead of invasive function parameters on
compileExpr.
compiled Plutus script, embedding package name, module name, and source location in
the certificate metadata.
(single pattern match instead of recursive go), and package name resolution
(lookupUnit / thisPackageName / stripVersionFromUnitId fallback chain).
createDirectoryIfMissing, remove noisy console output.
recover RealSrcSpan from the type-level string.
(scripts/plinth-certifier-tests.py).