From 95fc4cc7a0d0ab5354ad99754c5b3da742709238 Mon Sep 17 00:00:00 2001 From: tiye Date: Mon, 5 Jan 2026 10:06:16 +0800 Subject: [PATCH 1/5] add note --- README.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/README.md b/README.md index 87578ac..4961ec3 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,9 @@ # Idris2 Respo +> **⚠️ Experimental Project Notice** +> +> This is an experimental project generated with AI assistance for learning and exploration purposes. It demonstrates concepts from [rs-respo](https://github.com/Respo/rs.respo) ported to Idris2, but is **not production-ready** and should not be used in real-world applications. + Idris2 implementation of Respo, a virtual DOM library with effects system. This is a port of the core ideas from [rs-respo](https://github.com/Respo/rs.respo). ## Features From 1d08220a72143a3176db68ca5f688c5b75543502 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 5 Jan 2026 03:00:06 +0000 Subject: [PATCH 2/5] Initial plan From dd061ce66761f03174b41dbab6bd4a47094f5fad Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 5 Jan 2026 03:03:42 +0000 Subject: [PATCH 3/5] Clean up backup file and fix GitHub Actions configuration Co-authored-by: tiye <449224+tiye@users.noreply.github.com> --- .github/workflows/build-and-deploy.yaml | 6 +- .gitignore | 1 + src/Respo/Effect.idr.bak | 123 ------------------------ 3 files changed, 3 insertions(+), 127 deletions(-) delete mode 100644 src/Respo/Effect.idr.bak diff --git a/.github/workflows/build-and-deploy.yaml b/.github/workflows/build-and-deploy.yaml index 1b0a0fa..b029432 100644 --- a/.github/workflows/build-and-deploy.yaml +++ b/.github/workflows/build-and-deploy.yaml @@ -49,15 +49,13 @@ jobs: - name: Verify Idris2 run: | export PATH="/usr/local/bin:$HOME/.idris2/bin:$PATH" - export IDRIS2_PREFIX=/usr/local/idris2-0.8.0 idris2 --version - echo "IDRIS2_PREFIX set to: $IDRIS2_PREFIX" - ls -la $IDRIS2_PREFIX/support/js/ + echo "Idris2 installed at: $(which idris2)" + ls -la /usr/local/share/idris2-0.8.0/support/js/ || echo "JS support directory not found" - name: Build project run: | export PATH="/usr/local/bin:$HOME/.idris2/bin:$PATH" - export IDRIS2_PREFIX=/usr/local/idris2-0.8.0 idris2 --codegen javascript --build respo.ipkg - name: Prepare distribution diff --git a/.gitignore b/.gitignore index 26d7cdf..9744c4f 100644 --- a/.gitignore +++ b/.gitignore @@ -14,6 +14,7 @@ dist/ *.swp *.swo *~ +*.bak # OS .DS_Store diff --git a/src/Respo/Effect.idr.bak b/src/Respo/Effect.idr.bak deleted file mode 100644 index 656c07c..0000000 --- a/src/Respo/Effect.idr.bak +++ /dev/null @@ -1,123 +0,0 @@ -module Respo.Effect - -import Respo.Dom - -%default total - -public export -data EffectType = Mounted | BeforeUpdate | Updated | BeforeUnmount - -public export -Eq EffectType where - Mounted == Mounted = True - BeforeUpdate == BeforeUpdate = True - Updated == Updated = True - BeforeUnmount == BeforeUnmount = True - _ == _ = False - -public export -Show EffectType where - show Mounted = "mounted" - show BeforeUpdate = "beforeUpdate" - show Updated = "updated" - show BeforeUnmount = "beforeUnmount" - -public export -record RespoEffectWithData a where - constructor MkEffectWithData - effectId : String - effectData : a - onMounted : Maybe (a -> String -> IO ()) - onBeforeUpdate : Maybe (a -> String -> IO ()) - onUpdated : Maybe (a -> String -> IO ()) - onBeforeUnmount : Maybe (a -> String -> IO ()) - -public export -Eq a => Eq (RespoEffectWithData a) where - e1 == e2 = e1.effectId == e2.effectId - -public export -Show (RespoEffectWithData a) where - show eff = "Effect(" ++ eff.effectId ++ ")" - -public export -data AnyEffect : Type where - WrapEffect : Eq a => RespoEffectWithData a -> AnyEffect - -public export -Eq AnyEffect where - (WrapEffect e1) == (WrapEffect e2) = e1.effectId == e2.effectId - -public export -Show AnyEffect where - show (WrapEffect eff) = show eff - -public export -getEffectId : AnyEffect -> String -getEffectId (WrapEffect eff) = eff.effectId - -public export -RespoEffect : Type -RespoEffect = RespoEffectWithData () - -public export -MkEffect : String -> Maybe (String -> IO ()) -> Maybe (String -> IO ()) -> Maybe (String -> IO ()) -> Maybe (String -> IO ()) -> RespoEffect -MkEffect id onMount onBefore onUpdate onUnmount = MkEffectWithData id () (map (\f => \_, elId => f elId) onMount) (map (\f => \_, elId => f elId) onBefore) (map (\f => \_, elId => f elId) onUpdate) (map (\f => \_, elId => f elId) onUnmount) - -public export -effectMounted : String -> (String -> IO ()) -> RespoEffect -effectMounted id callback = MkEffect id (Just callback) Nothing Nothing Nothing - -public export -effectMountedWith : {a : _} -> Eq a => String -> a -> (a -> String -> IO ()) -> RespoEffectWithData a -effectMountedWith id data callback = MkEffectWithData id data (Just callback) Nothing Nothing Nothing - -public export -effectUpdated : String -> (String -> IO ()) -> RespoEffect -effectUpdated id callback = MkEffect id Nothing Nothing (Just callback) Nothing - -public export -effectUpdatedWith : {a : _} -> Eq a => String -> a -> (a -> String -> IO ()) -> RespoEffectWithData a -effectUpdatedWith id data callback = MkEffectWithData id data Nothing Nothing (Just callback) Nothing - -public export -effectMountedAndUpdated : String -> (String -> IO ()) -> (String -> IO ()) -> RespoEffect -effectMountedAndUpdated id onMount onUpdate = MkEffect id (Just onMount) Nothing (Just onUpdate) Nothing - -public export -effectMountedAndUpdatedWith : {a : _} -> Eq a => String -> a -> (a -> String -> IO ()) -> (a -> String -> IO ()) -> RespoEffectWithData a -effectMountedAndUpdatedWith id data onMount onUpdate = MkEffectWithData id data (Just onMount) Nothing (Just onUpdate) Nothing - -public export -effectFull : String -> Maybe (String -> IO ()) -> Maybe (String -> IO ()) -> Maybe (String -> IO ()) -> Maybe (String -> IO ()) -> RespoEffect -effectFull = MkEffect - -public export -effectFullWith : {a : _} -> Eq a => String -> a -> Maybe (a -> String -> IO ()) -> Maybe (a -> String -> IO ()) -> Maybe (a -> String -> IO ()) -> Maybe (a -> String -> IO ()) -> RespoEffectWithData a -effectFullWith = MkEffectWithData - -public export covering -runEffect : RespoEffect -> EffectType -> String -> IO () -runEffect eff Mounted elementId = case eff.onMounted of {Just callback => callback () elementId; Nothing => pure ()} -runEffect eff BeforeUpdate elementId = case eff.onBeforeUpdate of {Just callback => callback () elementId; Nothing => pure ()} -runEffect eff Updated elementId = case eff.onUpdated of {Just callback => callback () elementId; Nothing => pure ()} -runEffect eff BeforeUnmount elementId = case eff.onBeforeUnmount of {Just callback => callback () elementId; Nothing => pure ()} - -public export covering -runEffectWithData : RespoEffectWithData a -> EffectType -> String -> IO () -runEffectWithData eff Mounted elementId = case eff.onMounted of {Just callback => callback eff.effectData elementId; Nothing => pure ()} -runEffectWithData eff BeforeUpdate elementId = case eff.onBeforeUpdate of {Just callback => callback eff.effectData elementId; Nothing => pure ()} -runEffectWithData eff Updated elementId = case eff.onUpdated of {Just callback => callback eff.effectData elementId; Nothing => pure ()} -runEffectWithData eff BeforeUnmount elementId = case eff.onBeforeUnmount of {Just callback => callback eff.effectData elementId; Nothing => pure ()} - -public export covering -runAnyEffect : AnyEffect -> EffectType -> String -> IO () -runAnyEffect (WrapEffect eff) effType elementId = runEffectWithData eff effType elementId - -public export -toAnyEffect : RespoEffect -> AnyEffect -toAnyEffect = WrapEffect - -public export -wrapEffect : Eq a => RespoEffectWithData a -> AnyEffect -wrapEffect = WrapEffect From be44237ac6ede65dfb7b023ea61960205a9ee225 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 5 Jan 2026 04:25:06 +0000 Subject: [PATCH 4/5] Use idris2-pack Docker container for reliable builds Co-authored-by: tiye <449224+tiye@users.noreply.github.com> --- .github/workflows/build-and-deploy.yaml | 37 +++---------------------- 1 file changed, 4 insertions(+), 33 deletions(-) diff --git a/.github/workflows/build-and-deploy.yaml b/.github/workflows/build-and-deploy.yaml index b029432..7021197 100644 --- a/.github/workflows/build-and-deploy.yaml +++ b/.github/workflows/build-and-deploy.yaml @@ -12,50 +12,21 @@ jobs: runs-on: ubuntu-latest permissions: contents: read + # Use idris2-pack container which has Idris2 pre-installed with all dependencies + container: ghcr.io/stefan-hoeck/idris2-pack:latest + env: + PACK_DIR: /root/.pack steps: - uses: actions/checkout@v4 - - name: Cache Idris2 - uses: actions/cache@v3 - id: cache-idris2 - with: - path: | - ~/.idris2 - /usr/local/bin/idris2 - /usr/local/bin/idris2_app - /usr/local/share/idris2-0.8.0 - /usr/local/lib/idris2-0.8.0 - key: idris2-0.8.0-full-${{ runner.os }} - - - name: Install dependencies - if: steps.cache-idris2.outputs.cache-hit != 'true' - run: | - sudo apt-get update - sudo apt-get install -y chezscheme libgmp-dev - - - name: Install Idris2 - if: steps.cache-idris2.outputs.cache-hit != 'true' - run: | - git clone https://github.com/idris-lang/Idris2.git - cd Idris2 - git checkout v0.8.0 - make bootstrap SCHEME=scheme - sudo make install PREFIX=/usr/local - sudo make install-api PREFIX=/usr/local - cd .. - rm -rf Idris2 - - name: Verify Idris2 run: | - export PATH="/usr/local/bin:$HOME/.idris2/bin:$PATH" idris2 --version echo "Idris2 installed at: $(which idris2)" - ls -la /usr/local/share/idris2-0.8.0/support/js/ || echo "JS support directory not found" - name: Build project run: | - export PATH="/usr/local/bin:$HOME/.idris2/bin:$PATH" idris2 --codegen javascript --build respo.ipkg - name: Prepare distribution From 3433f980952c416e6e1ecc15a600145c12c641ab Mon Sep 17 00:00:00 2001 From: tiye Date: Mon, 5 Jan 2026 13:29:23 +0800 Subject: [PATCH 5/5] remote branch filter in actions --- .github/workflows/build-and-deploy.yaml | 2 -- 1 file changed, 2 deletions(-) diff --git a/.github/workflows/build-and-deploy.yaml b/.github/workflows/build-and-deploy.yaml index 7021197..3d2c7ce 100644 --- a/.github/workflows/build-and-deploy.yaml +++ b/.github/workflows/build-and-deploy.yaml @@ -38,7 +38,6 @@ jobs: ls -la dist/ - name: Deploy to server - if: github.event_name == 'push' && github.ref == 'refs/heads/main' id: deploy uses: Pendect/action-rsyncer@v2.0.0 env: @@ -51,5 +50,4 @@ jobs: dest: "rsync-user@tiye.me:/web-assets/repo/${{ github.repository }}" - name: Display status from deploy - if: github.event_name == 'push' && github.ref == 'refs/heads/main' run: echo "${{ steps.deploy.outputs.status }}"