diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -91,6 +91,13 @@
 phino --pin=0.0.0.67 dataize hello.phi
 ```
 
+The `--pin-file` global option does the same, but reads the version from
+a file, ignoring the whitespace around it:
+
+```bash
+phino --pin-file=version.txt dataize hello.phi
+```
+
 ## Dataize
 
 Then, you dataize the expression:
diff --git a/phino.cabal b/phino.cabal
--- a/phino.cabal
+++ b/phino.cabal
@@ -1,6 +1,6 @@
 cabal-version: 3.0
 name: phino
-version: 0.0.139
+version: 0.0.140
 license: MIT
 synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions
 description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>
diff --git a/src/CLI.hs b/src/CLI.hs
--- a/src/CLI.hs
+++ b/src/CLI.hs
@@ -11,7 +11,10 @@
 import CLI.Runners
 import CLI.Types
 import Control.Exception.Base (SomeException, fromException, handle, throwIO)
+import Data.Char (isSpace)
+import Data.List (dropWhileEnd)
 import Data.Version (showVersion)
+import Files (ensuredFile)
 import Logger
 import Options.Applicative
 import Paths_phino (version)
@@ -66,9 +69,10 @@
             CmdMerge OptsMerge{_logLevel, _logLines} -> (_logLevel, _logLines)
             CmdMatch OptsMatch{_logLevel, _logLines} -> (_logLevel, _logLines)
        in setLogConfig level lns
-    checkPin :: Maybe String -> IO ()
+    checkPin :: Maybe Pin -> IO ()
     checkPin Nothing = pure ()
-    checkPin (Just expected)
+    checkPin (Just (PinFile file)) = ensuredFile file >>= readFile >>= checkPin . Just . PinVersion . dropWhileEnd isSpace . dropWhile isSpace
+    checkPin (Just (PinVersion expected))
       | expected == actual = pure ()
       | otherwise = throwIO (VersionMismatch expected actual)
       where
diff --git a/src/CLI/Parsers.hs b/src/CLI/Parsers.hs
--- a/src/CLI/Parsers.hs
+++ b/src/CLI/Parsers.hs
@@ -512,15 +512,23 @@
         <> command "match" (info matchParser (progDesc "Match 𝜑-expression against provided pattern and build matched substitutions"))
     )
 
-optPin :: Parser (Maybe String)
-optPin =
-  optional
-    ( strOption
+optPin :: Parser (Maybe Pin)
+optPin = optional (PinVersion <$> literal <|> PinFile <$> file)
+  where
+    literal :: Parser String
+    literal =
+      strOption
         ( long "pin"
             <> metavar "VERSION"
             <> help "Fail if this version doesn't match the version of phino"
         )
-    )
+    file :: Parser FilePath
+    file =
+      strOption
+        ( long "pin-file"
+            <> metavar "FILE"
+            <> help "Fail if the version written in this file doesn't match the version of phino"
+        )
 
 cliArgsParser :: Parser CliArgs
 cliArgsParser = CliArgs <$> optPin <*> commandParser
diff --git a/src/CLI/Types.hs b/src/CLI/Types.hs
--- a/src/CLI/Types.hs
+++ b/src/CLI/Types.hs
@@ -64,8 +64,10 @@
   | CmdMerge OptsMerge
   | CmdMatch OptsMatch
 
+data Pin = PinVersion String | PinFile FilePath
+
 data CliArgs = CliArgs
-  { _pin :: Maybe String
+  { _pin :: Maybe Pin
   , _command :: Command
   }
 
diff --git a/src/Morph.hs b/src/Morph.hs
--- a/src/Morph.hs
+++ b/src/Morph.hs
@@ -450,21 +450,19 @@
 -- allows. Every entry is charged to the '--max-steps' budget, which is what
 -- bounds the walk.
 deepened :: Expression -> Expression -> State -> ReduceContext -> IO (Expression, State)
-deepened expr univ state ctx = go False (Just ctx._site) Nothing ExXi expr state ctx
+deepened expr univ state ctx = go (Just ctx._site) Nothing ExXi expr state ctx
   where
     -- A term as it was written, together with the locator naming it where one
     -- does and with what its free ξ stands for: the formation the walk entered
     -- it from, without the binding it came from, exactly the context the 'dot'
     -- rule hands a dispatched body. At the top there is no such formation, so ξ
     -- stands for itself and contextualization leaves the term alone, and the
-    -- locator is the one the whole run was aimed at. Whether the formation a
-    -- term is bound in has its ρ bound is what decides whether a void ρ keeps
-    -- a formation from being entered (see 'parts'); at the top there is none.
-    go :: Bool -> Maybe Expression -> Maybe Attribute -> Expression -> Expression -> State -> ReduceContext -> IO (Expression, State)
-    go attached standing dispatched context term state' caller = do
+    -- locator is the one the whole run was aimed at.
+    go :: Maybe Expression -> Maybe Attribute -> Expression -> Expression -> State -> ReduceContext -> IO (Expression, State)
+    go standing dispatched context term state' caller = do
       let here = sited standing caller
       ctx' <- deeper here
-      (walked, walkedState) <- parts attached standing context term state' here
+      (walked, walkedState) <- parts standing context term state' here
       (answer, answered) <- ctx'._fire dispatched (contextualize walked context) univ walkedState ctx'
       pure (fromMaybe walked answer, answered)
     -- The context a term is walked in, aimed at the term itself where a locator
@@ -482,32 +480,29 @@
     -- formation, one holding a void, is a method nobody applied: its body is
     -- parametric, walking it can only end in ⊥ or a stuck term, and a λ there
     -- dataizing a parameter would end the whole run, so it is handed back as it
-    -- was written (#1393). A void ρ counts as well where the formation it is
-    -- bound in has its own ρ bound: ρ is the parameter a dispatch binds, and
-    -- 'dot' binds it in every copy a reduction reaches, so a formation still
-    -- holding ρ ↦ ∅ inside such a copy is a method nobody dispatched, and its
-    -- ξ.ρ can only collapse to ⊥ (#1397). In the program as it was written
-    -- nothing is dispatched yet, so the void ρ an object declares there keeps
-    -- it from nothing and its objects are walked the way they always were.
-    parts :: Bool -> Maybe Expression -> Expression -> Expression -> State -> ReduceContext -> IO (Expression, State)
-    parts attached _ _ term@(ExFormation bds) state' _
+    -- was written (#1393). A void ρ counts like any other: a formation holds
+    -- one only where the program declared it, so it is a method waiting for
+    -- the receiver a dispatch hands it, and its ξ.ρ can only collapse to ⊥
+    -- wherever it stands, in a copy that kept its ρ or in one 'skip' dropped
+    -- it from (#1397, #1414).
+    parts :: Maybe Expression -> Expression -> Expression -> State -> ReduceContext -> IO (Expression, State)
+    parts _ _ term@(ExFormation bds) state' _
       | any abstract bds = pure (term, state')
       where
         abstract :: Binding -> Bool
-        abstract (BiVoid AtRho) = attached
         abstract (BiVoid _) = True
         abstract _ = False
-    parts _ standing _ (ExFormation bds) state' caller = do
+    parts standing _ (ExFormation bds) state' caller = do
       (entered, state'') <- bindings standing bds bds state' caller
       pure (ExFormation entered, state'')
-    parts _ _ context (ExDispatch target attr) state' caller = do
-      (entered, state'') <- go False Nothing (Just attr) context target state' caller
+    parts _ context (ExDispatch target attr) state' caller = do
+      (entered, state'') <- go Nothing (Just attr) context target state' caller
       pure (ExDispatch entered attr, state'')
-    parts _ _ context (ExApplication target arg) state' caller = do
-      (entered, state'') <- go False Nothing Nothing context target state' caller
+    parts _ context (ExApplication target arg) state' caller = do
+      (entered, state'') <- go Nothing Nothing context target state' caller
       (applied, state''') <- argument context arg state'' caller
       pure (ExApplication entered applied, state''')
-    parts _ _ _ term state' _ = pure (term, state')
+    parts _ _ term state' _ = pure (term, state')
     -- Walk the bindings of a formation left to right, threading the state
     -- through them. Only what the formation itself holds is entered: ρ names
     -- the object around it rather than one inside it, and a void, Δ or λ
@@ -518,13 +513,9 @@
     bindings _ _ [] state' _ = pure ([], state')
     bindings standing whole (BiTau attr body : rest) state' caller
       | attr /= AtRho = do
-          (entered, state'') <- go (any bound whole) (fmap (`ExDispatch` attr) standing) Nothing (scope attr whole) body state' caller
+          (entered, state'') <- go (fmap (`ExDispatch` attr) standing) Nothing (scope attr whole) body state' caller
           (others, state''') <- bindings standing whole rest state'' caller
           pure (BiTau attr entered : others, state''')
-      where
-        bound :: Binding -> Bool
-        bound (BiTau AtRho _) = True
-        bound _ = False
     bindings standing whole (bd : rest) state' caller = do
       (others, state'') <- bindings standing whole rest state' caller
       pure (bd : others, state'')
@@ -541,10 +532,10 @@
     -- applies is walked by the caller and the argument it binds is walked here.
     argument :: Expression -> Argument -> State -> ReduceContext -> IO (Argument, State)
     argument context (ArTau attr arg) state' caller = do
-      (entered, state'') <- go False Nothing Nothing context arg state' caller
+      (entered, state'') <- go Nothing Nothing context arg state' caller
       pure (ArTau attr entered, state'')
     argument context (ArAlpha alpha arg) state' caller = do
-      (entered, state'') <- go False Nothing Nothing context arg state' caller
+      (entered, state'') <- go Nothing Nothing context arg state' caller
       pure (ArAlpha alpha entered, state'')
 
 -- The premise binding the given expression meta, if any. The conclusion of a
diff --git a/test/CLISpec.hs b/test/CLISpec.hs
--- a/test/CLISpec.hs
+++ b/test/CLISpec.hs
@@ -161,6 +161,48 @@
       ]
       (\(desc, args, test, expected) -> it desc (withStdin "[[ ]]" (test args expected)))
 
+  describe "--pin-file" $
+    forM_
+      [
+        ( "succeeds when --pin-file holds actual version among spaces"
+        , Just ("  \n" ++ showVersion version ++ " \t\n\n")
+        , testCLISucceeded
+        , ["⟦⟧"]
+        )
+      ,
+        ( "fails when --pin-file holds another version"
+        , Just "7.3.0.41\n"
+        , testCLIFailed
+        , ["Version mismatch: --pin requires '7.3.0.41', but this is phino " ++ showVersion version]
+        )
+      ,
+        ( "fails when --pin-file is empty"
+        , Just " \n"
+        , testCLIFailed
+        , ["Version mismatch: --pin requires ''"]
+        )
+      ,
+        ( "fails when --pin-file is absent"
+        , Nothing
+        , testCLIFailed
+        , ["does not exist"]
+        )
+      ]
+      ( \(desc, content, test, expected) ->
+          it desc $
+            withTempDirectory "phino-pin-file" $ \dir -> do
+              createDirectoryIfMissing True dir
+              let file = dir </> "vérsion.txt"
+              forM_ content (writeFile file)
+              withStdin "[[ ]]" (test ["--pin-file=" ++ file, "rewrite", "--sweet"] expected)
+      )
+
+  it "fails when both --pin and --pin-file are given" $
+    withStdin "[[ ]]" $
+      testCLIFailed
+        ["--pin=" ++ showVersion version, "--pin-file=pinned-version.txt", "rewrite"]
+        ["[ERROR]"]
+
   describe "--hide-rho" $
     forM_
       [