Remove certifier from plutus-tx-plugin (#7390)

* Remove certifier from plutus-tx-plugin

* Add changelog

Author: ana-pantilie

plutus-tx-plugin/changelog.d/20251016_172209_ana.pantilie95_remove_certifier_from_plugin.md

@@ -0,0 +1,4 @@
+### Removed
+
+- Removed the experimental compiler certification option temporarily due to ghc issues regarding the profiling build of `plutus-metatheory`.
+

plutus-tx-plugin/plutus-tx-plugin.cabal

@@ -82,12 +82,10 @@ library
     , extra
     , ghc
     , lens
-    , megaparsec
     , mtl
     , plutus-core            ^>=1.54
     , plutus-core:flat
     , plutus-core:plutus-ir
-    , plutus-metatheory      ^>=1.54
     , plutus-tx              ^>=1.54
     , prettyprinter
     , template-haskell

plutus-tx-plugin/src/PlutusTx/Options.hs

@@ -19,7 +19,6 @@ import PlutusIR.Compiler.Types qualified as PIR
 import PlutusTx.Compiler.Types
 import UntypedPlutusCore qualified as UPLC
 
-import Control.Applicative (many, optional, (<|>))
 import Control.Exception
 import Control.Lens
 import Data.Bifunctor (first)
@@ -36,7 +35,6 @@ import Data.Text qualified as Text
 import Data.Type.Equality
 import GHC.Plugins qualified as GHC
 import Prettyprinter
-import Text.Megaparsec.Char (alphaNumChar, char, upperChar)
 
 import Text.Read (readMaybe)
 import Type.Reflection
@@ -78,7 +76,6 @@ data PluginOptions = PluginOptions
     -- Which effectively ignores the trace text.
     _posRemoveTrace                    :: Bool
   , _posDumpCompilationTrace           :: Bool
-  , _posCertify                        :: Maybe String
   }
 
 makeLenses ''PluginOptions
@@ -310,18 +307,6 @@ pluginOptions =
     , let k = "dump-compilation-trace"
           desc = "Dump compilation trace for debugging"
        in (k, PluginOption typeRep (setTrue k) posDumpCompilationTrace desc [])
-    , let k = "certify"
-          desc =
-            "Produce a certificate for the compiled program, with the given name. "
-              <> "This certificate provides evidence that the compiler optimizations have "
-              <> "preserved the functional behavior of the original program. "
-              <> "Currently, this is only supported for the UPLC compilation pipeline. "
-              <> "Warning: this is an experimental feature and may not work as expected."
-          p = optional $ do
-            firstC <- upperChar
-            rest <- many (alphaNumChar <|> char '_' <|> char '\\')
-            pure (firstC : rest)
-       in (k, PluginOption typeRep (plcParserOption p k) posCertify desc [])
     ]
 
 flag :: (a -> a) -> OptionKey -> Maybe OptionValue -> Validation ParseError (a -> a)
@@ -394,7 +379,6 @@ defaultPluginOptions =
     , _posPreserveLogging = True
     , _posRemoveTrace = False
     , _posDumpCompilationTrace = False
-    , _posCertify = Nothing
     }
 
 processOne

plutus-tx-plugin/src/PlutusTx/Plugin.hs

@@ -83,11 +83,9 @@ import PlutusIR.Compiler.Types qualified as PIR
 import PlutusIR.Transform.RewriteRules
 import PlutusIR.Transform.RewriteRules.RemoveTrace (rewriteRuleRemoveTrace)
 import Prettyprinter qualified as PP
-import System.IO (hPutStrLn, openBinaryTempFile, stderr)
+import System.IO (openBinaryTempFile)
 import System.IO.Unsafe (unsafePerformIO)
 
-import Certifier
-
 data PluginCtx = PluginCtx
   { pcOpts            :: PluginOptions
   , pcFamEnvs         :: GHC.FamInstEnvs
@@ -638,17 +636,7 @@ runCompiler moduleName opts expr = do
         modifyError PLC.TypeErrorE $
           PLC.inferTypeOfProgram plcTcConfig (plcP $> annMayInline)
 
-  let optCertify = opts ^. posCertify
-  (uplcP, simplTrace) <- flip runReaderT plcOpts $ PLC.compileProgramWithTrace plcP
-  liftIO $ case optCertify of
-      Just certName -> do
-          result <- runCertifier $ mkCertifier simplTrace certName
-          case result of
-              Right certSuccess ->
-                  hPutStrLn stderr $ prettyCertifierSuccess certSuccess
-              Left err ->
-                 hPutStrLn stderr $ prettyCertifierError err
-      Nothing -> pure ()
+  (uplcP, _) <- flip runReaderT plcOpts $ PLC.compileProgramWithTrace plcP
   dbP <- liftExcept $ modifyError PLC.FreeVariableErrorE $ traverseOf UPLC.progTerm UPLC.deBruijnTerm uplcP
   when (opts ^. posDumpUPlc) . liftIO $
       dumpFlat