Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3, actions/setup-python@v1, actions/cache@v3, actions/upload-artifact@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.

The following actions uses node12 which is deprecated and will be forced to run on node16: actions/setup-python@v1. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/

/home/runner/work/lean-ga/lean-ga/src/geometric_algebra/translations/ida_derived.lean:45:0: declaration 'ida'.rvector_mul' uses sorry

/home/runner/work/lean-ga/lean-ga/src/geometric_algebra/translations/ida_derived.lean:59:0: declaration 'ida'.multivector.ring' uses sorry

/home/runner/work/lean-ga/lean-ga/src/geometric_algebra/translations/hol_light.lean:65:0: declaration 'hol.wedge.assoc' uses sorry

/home/runner/work/lean-ga/lean-ga/src/geometric_algebra/from_mathlib/basic.lean:50:0: declaration '[anonymous]' uses sorry

/home/runner/work/lean-ga/lean-ga/src/geometric_algebra/translations/ida_derived.lean:60:0: declaration 'ida'.multivector.algebra' uses sorry

/home/runner/work/lean-ga/lean-ga/src/geometric_algebra/translations/ida.lean:82:0: declaration 'ida.multivector.has_mul' uses sorry

/home/runner/work/lean-ga/lean-ga/src/geometric_algebra/translations/ida.lean:89:0: declaration 'ida.multivector.ring' uses sorry

/home/runner/work/lean-ga/lean-ga/src/geometric_algebra/translations/ida.lean:91:0: declaration 'ida.multivector.algebra' uses sorry

/home/runner/work/lean-ga/lean-ga/src/geometric_algebra/from_mathlib/contract.lean:39:0: declaration 'clifford_algebra.change_form_reverse' uses sorry

/home/runner/work/lean-ga/lean-ga/src/geometric_algebra/from_mathlib/default.lean:2:0: imported file '/home/runner/work/lean-ga/lean-ga/src/geometric_algebra/from_mathlib/conjugation.lean' uses sorry

/home/runner/work/lean-ga/lean-ga/src/geometric_algebra/translations/laurents.lean:80:0: (a + b)⋎(a⋏b) : Gₙ α 2

/home/runner/work/lean-ga/lean-ga/src/geometric_algebra/nursery/chisolm.lean:163:0: 2 + ↑v : multivector 1