# Changelog for refinery

• 0.4.0.0
• How failure is handled has been refined somewhat. Previously, if a tactic failed, then the extraction process was terminated, and proofs would return a Left describing the error. This design worked, but led to some suboptimal error reporting. To fix this, the Failure constructor from ProofStateT has been changed from

| Failure err


to

| Failure err (ext' -> ProofStateT ext' ext err s m goal)


This allows us the option to continue the extraction process even in the face of failure. This option is exercised in partialProofs and runPartialTacticT.

• A bunch of helpful combinators have been added for extract manipulation inside of tactics.

• proofs no longer returns a tuple, but rather a record type

data Proof s meta goal ext = Proof { pf_extract :: ext, pf_state :: s, pf_unsolvedGoals :: [(meta, goal)] }

• Added handler, and removed the MonadError instance for TacticT. Now, instead of recovering from errors (which was fraught with subtle issues), we allow the user to annotate errors instead.

• Added some useful tactic combinators:

• tweak
• peek
• poke
• inspect
• some_
• Swapped the order of arguments to mapExtract to line up with Profunctor

• Reworked MonadExtract to support named holes.

• Added reify and resume combinators, which are used for inspecting the current proof state during tactic execution.

• 0.3.0.0
• Reworked the core types of the library, which fixed a lot of the weird behavior that users were experiencing.
• 0.2.0.0
• Added Alternative/MonadPlus instances to ProofStateT, TacticT, RuleT
• 0.1.0.0
• Initial Release of the library