darcsweb - test/Spec.hs

module Main where

import System.Process (callCommand)
import System.Exit (exitFailure, exitSuccess)
import Control.Exception (try, SomeException)
import qualified Properties.Html as Html

main :: IO ()
main = do
    -- Phase 1: Verify Rocq/Coq proofs
    putStrLn "=== Verifying Rocq proofs ==="
    proofResult <- try (callCommand "make -C verified proofs")
                   :: IO (Either SomeException ())
    case proofResult of
      Left e -> do
        putStrLn $ "Proof verification failed: " ++ show e
        exitFailure
      Right () ->
        putStrLn "All proofs verified."

    -- Phase 2: Run QuickCheck property tests
    putStrLn "\n=== Running QuickCheck properties ==="
    ok <- Html.tests
    if ok
      then do
        putStrLn "\nAll properties passed."
        exitSuccess
      else do
        putStrLn "\nSome properties FAILED."
        exitFailure