From b157b0017456dfbed225437132fcb66fd7ac69cb Mon Sep 17 00:00:00 2001 From: Nicolas Biri Date: Mon, 22 Dec 2025 20:32:37 +0100 Subject: [PATCH 1/2] Tidy up code --- src/Replica/App/Log.idr | 1 - src/Replica/App/Run.idr | 4 ++-- src/Replica/App/Set.idr | 1 - src/Replica/Command/Help.idr | 2 ++ 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Replica/App/Log.idr b/src/Replica/App/Log.idr index 7c02228..8248a56 100644 --- a/src/Replica/App/Log.idr +++ b/src/Replica/App/Log.idr @@ -5,7 +5,6 @@ import Control.App.Console import Replica.App.Replica import Replica.Option.Global -import Replica.Other.Decorated %default total diff --git a/src/Replica/App/Run.idr b/src/Replica/App/Run.idr index f7a70a0..c33c102 100644 --- a/src/Replica/App/Run.idr +++ b/src/Replica/App/Run.idr @@ -35,7 +35,7 @@ import Replica.Other.Validation %default total --- Create the folders needed by Replica (usually ./.replica/test and ./.replica/log) +-- Create the folders needed by Replica (with default settings ./.replica/test and ./.replica/log) prepareReplicaDir : SystemIO (SystemError :: e) => FileSystem (FSError :: e) => Has [ State RunContext RunCommand @@ -64,6 +64,7 @@ prepareReplicaDir = do data RunType = Partial | Total +-- Specifies the tests to run data RunningPlan = None | Running RunType SuitePlan TestPlan @@ -111,7 +112,6 @@ runAllTests plan = do batchTests [] plan where - handleInaccessibleTests : List (Test, Either TestError TestResult) -> SuitePlan -> App e (Maybe SuitePlan, List (Test, Either TestError TestResult)) diff --git a/src/Replica/App/Set.idr b/src/Replica/App/Set.idr index e3f9ce9..f8a6d65 100644 --- a/src/Replica/App/Set.idr +++ b/src/Replica/App/Set.idr @@ -40,7 +40,6 @@ updateConfig = updateConfig' [] else updateConfig' (x :: xs) ys s - export setReplica : FileSystem (FSError :: e) => diff --git a/src/Replica/Command/Help.idr b/src/Replica/Command/Help.idr index ad82bc8..6470551 100644 --- a/src/Replica/Command/Help.idr +++ b/src/Replica/Command/Help.idr @@ -13,6 +13,8 @@ import public Replica.Help import Replica.Option.Types import Replica.Other.Validation +%default total + export help : Help help = MkHelp From 750b2f436a26f2a887f572d36abac9f07fc1ae12 Mon Sep 17 00:00:00 2001 From: Nicolas Biri Date: Mon, 22 Dec 2025 20:35:11 +0100 Subject: [PATCH 2/2] Update README install --- README.md | 7 ++----- documentation/README_JSON.md | 7 ++----- 2 files changed, 4 insertions(+), 10 deletions(-) diff --git a/README.md b/README.md index 526ff1f..b8afaaf 100644 --- a/README.md +++ b/README.md @@ -101,14 +101,11 @@ with `nix run github:replicatest/replica`. #### Requirements -- [idris2](https://idris-lang.org) (v0.6.0); +- [idris2](https://idris-lang.org) (v0.8.0); - [git](https://git-scm.com); - [dhall][] and [dhall-to-json][]. -Idris2 dependencies: - -- the [`papers`](https://github.com/idris-lang/Idris2/tree/main/libs/papers) - package. +Idris2 dependencies: None #### Steps diff --git a/documentation/README_JSON.md b/documentation/README_JSON.md index 1bd6987..5c2c479 100644 --- a/documentation/README_JSON.md +++ b/documentation/README_JSON.md @@ -101,13 +101,10 @@ You can either reuse it as an input to your own `flake`s or use it directly with #### Requirements -- [idris2](https://idris-lang.org) (v0.6.0); +- [idris2](https://idris-lang.org) (v0.8.0); - [git](https://git-scm.com); -Idris2 dependencies: - -- the [`papers`](https://github.com/idris-lang/Idris2/tree/main/libs/papers) - package. +Idris2 dependencies: None. ```shell # clone repo