Merge remote-tracking branch 'upstream/main' into rapid
430 files changed, 14666 insertions(+), 4710 deletions(-) M .github/linters/.markdown-lint.yml M .github/workflows/ci-idris2.yml M CHANGELOG.md M CONTRIBUTING.md M CONTRIBUTORS M INSTALL.md M Makefile M bootstrap-stage2.sh M bootstrap/idris2_app/idris2.rkt M docs/source/backends/custom.rst M docs/source/backends/index.rst A docs/source/cookbook/Calculator.idr A docs/source/cookbook/LambdaCalculus.idr A docs/source/cookbook/index.rst A docs/source/cookbook/parsing.rst M docs/source/implementation/ide-protocol.rst M docs/source/index.rst M docs/source/tutorial/interactive.rst M docs/source/tutorial/interfaces.rst M docs/source/tutorial/modules.rst M docs/source/tutorial/packages.rst M idris2api.ipkg M libs/base/Control/Function.idr M libs/base/Control/Monad/Error/Interface.idr M libs/base/Control/Monad/RWS/CPS.idr M libs/base/Control/Monad/Writer/Interface.idr M libs/base/Data/Fin.idr M libs/base/Data/List.idr M libs/base/Data/List/Elem.idr M libs/base/Data/List1.idr A libs/base/Data/List1/Elem.idr M libs/base/Data/List1/Properties.idr A libs/base/Data/List1/Quantifiers.idr M libs/base/Data/Nat.idr M libs/base/Data/SnocList.idr M libs/base/Data/SnocList/Elem.idr M libs/base/Data/So.idr M libs/base/Data/String.idr M libs/base/Data/These.idr M libs/base/Data/Vect.idr M libs/base/Data/Vect/Quantifiers.idr M libs/base/Decidable/Equality.idr M libs/base/Decidable/Equality/Core.idr A libs/base/Deriving/Common.idr A libs/base/Deriving/Foldable.idr A libs/base/Deriving/Functor.idr A libs/base/Deriving/Traversable.idr M libs/base/Language/Reflection.idr M libs/base/Language/Reflection/TT.idr M libs/base/Language/Reflection/TTImp.idr M libs/base/System.idr M libs/base/System/Clock.idr M libs/base/System/Concurrency.idr M libs/base/System/Directory.idr M libs/base/System/FFI.idr M libs/base/System/File/ReadWrite.idr M libs/base/System/Signal.idr M libs/base/base.ipkg M libs/contrib/Data/List/Equalities.idr M libs/contrib/Data/List/Palindrome.idr M libs/contrib/Data/String/Extra.idr M libs/contrib/Data/Validated.idr M libs/contrib/Text/Lexer/Core.idr M libs/contrib/Text/Parser/Core.idr M libs/contrib/contrib.ipkg R libs/{contrib/Control/Linear/LIO.idr => linear/Control/Linear/LIO.idr} M libs/linear/linear.ipkg M libs/network/Control/Linear/Network.idr M libs/network/network.ipkg A libs/papers/Data/W.idr A libs/papers/Search/Auto.idr A libs/papers/Search/CTL.idr A libs/papers/Search/GCL.idr M libs/papers/Search/Generator.idr M libs/papers/Search/HDecidable.idr M libs/papers/Search/Properties.idr M libs/papers/papers.ipkg M libs/prelude/Builtin.idr M libs/prelude/Prelude/Cast.idr M libs/prelude/Prelude/IO.idr M libs/prelude/Prelude/Interfaces.idr M libs/prelude/Prelude/Types.idr M libs/prelude/PrimIO.idr M libs/test/Test/Golden.idr M src/Algebra/ZeroOneOmega.idr M src/Compiler/Common.idr M src/Compiler/CompileExpr.idr M src/Compiler/ES/Ast.idr M src/Compiler/ES/Codegen.idr M src/Compiler/ES/Doc.idr M src/Compiler/ES/Javascript.idr M src/Compiler/ES/Node.idr M src/Compiler/ES/ToAst.idr M src/Compiler/Inline.idr M src/Compiler/Interpreter/VMCode.idr M src/Compiler/LambdaLift.idr M src/Compiler/NoMangle.idr M src/Compiler/Opts/ConstantFold.idr M src/Compiler/RefC/RefC.idr M src/Compiler/Scheme/Chez.idr M src/Compiler/Scheme/ChezSep.idr M src/Compiler/Scheme/Gambit.idr M src/Compiler/Scheme/Racket.idr M src/Core/Binary.idr M src/Core/CompileExpr.idr M src/Core/Context.idr M src/Core/Context/Context.idr A src/Core/Context/TTC.idr M src/Core/Core.idr M src/Core/Env.idr M src/Core/Hash.idr M src/Core/Metadata.idr M src/Core/Normalise/Eval.idr M src/Core/Options.idr M src/Core/Options/Log.idr M src/Core/TT.idr A src/Core/TT/Views.idr M src/Core/TTC.idr M src/Core/Value.idr M src/Idris/CommandLine.idr M src/Idris/Desugar.idr M src/Idris/Desugar/Mutual.idr M src/Idris/Doc/Keywords.idr M src/Idris/Doc/String.idr M src/Idris/Elab/Implementation.idr M src/Idris/Error.idr M src/Idris/IDEMode/CaseSplit.idr M src/Idris/IDEMode/Holes.idr M src/Idris/IDEMode/REPL.idr M src/Idris/IDEMode/SyntaxHighlight.idr M src/Idris/ModTree.idr M src/Idris/Package.idr M src/Idris/Package/Types.idr M src/Idris/Parser.idr M src/Idris/ProcessIdr.idr M src/Idris/REPL.idr M src/Idris/REPL/Common.idr M src/Idris/REPL/FuzzySearch.idr M src/Idris/Resugar.idr M src/Idris/SetOptions.idr M src/Idris/Syntax.idr A src/Idris/Syntax/Pragmas.idr A src/Idris/Syntax/TTC.idr M src/Idris/Syntax/Traversals.idr M src/Libraries/Text/Lexer/Core.idr M src/Libraries/Text/Parser/Core.idr M src/Protocol/IDE/Command.idr M src/Protocol/IDE/Result.idr M src/Protocol/SExp.idr M src/TTImp/Elab/Ambiguity.idr M src/TTImp/Elab/Local.idr M src/TTImp/Elab/Quote.idr M src/TTImp/Elab/Rewrite.idr M src/TTImp/Elab/RunElab.idr M src/TTImp/Interactive/CaseSplit.idr A src/TTImp/Interactive/Completion.idr M src/TTImp/Interactive/ExprSearch.idr A src/TTImp/Interactive/Intro.idr M src/TTImp/Parser.idr M src/TTImp/ProcessData.idr M src/TTImp/ProcessDecls.idr M src/TTImp/ProcessRecord.idr M src/TTImp/ProcessRunElab.idr M src/TTImp/ProcessType.idr M src/TTImp/Reflect.idr M src/TTImp/TTImp.idr M src/TTImp/TTImp/Functor.idr A src/TTImp/TTImp/TTC.idr A src/TTImp/TTImp/Traversals.idr M src/TTImp/Unelab.idr M src/TTImp/Utils.idr M support/c/getline.c M support/c/getline.h M support/c/idris_directory.c M support/c/idris_directory.h M support/c/idris_file.c M support/c/idris_file.h M support/c/idris_memory.c M support/c/idris_memory.h M support/c/idris_signal.c M support/c/idris_support.c M support/c/idris_support.h M support/c/idris_system.c M support/c/idris_system.h M support/c/idris_term.c M support/c/idris_util.c M support/c/idris_util.h M support/c/windows/win_hack.c M support/c/windows/win_utils.c M support/c/windows/win_utils.h M support/gambit/support.scm M support/js/support.js A support/js/support_system_signal.js M support/racket/support.rkt M support/refc/buffer.c M support/refc/buffer.h M support/refc/casts.c M support/refc/casts.h M support/refc/clock.c M support/refc/conCaseHelper.c M support/refc/conCaseHelper.h M support/refc/mathFunctions.c M support/refc/mathFunctions.h M support/refc/memoryManagement.h M support/refc/prim.c M support/refc/prim.h M support/refc/refc_util.c M support/refc/refc_util.h M support/refc/stringOps.c M support/refc/stringOps.h M tests/Main.idr M tests/allbackends/basic048/Module'.idr M tests/allbackends/basic048/expected R tests/{chez/channels001/Main.idr => allschemes/channels001/Main.idr} R tests/{chez/channels001/expected => allschemes/channels001/expected} A tests/allschemes/channels001/run R tests/{chez/channels002/Main.idr => allschemes/channels002/Main.idr} R tests/{chez/channels002/expected => allschemes/channels002/expected} R tests/{chez/channels001/run => allschemes/channels002/run} R tests/{chez/channels003/Main.idr => allschemes/channels003/Main.idr} R tests/{chez/channels003/expected => allschemes/channels003/expected} R tests/{chez/channels002/run => allschemes/channels003/run} R tests/{chez/channels004/Main.idr => allschemes/channels004/Main.idr} R tests/{chez/channels004/expected => allschemes/channels004/expected} R tests/{chez/channels003/run => allschemes/channels004/run} R tests/{chez/channels005/Main.idr => allschemes/channels005/Main.idr} R tests/{chez/channels005/expected => allschemes/channels005/expected} R tests/{chez/channels004/run => allschemes/channels005/run} A tests/allschemes/channels006/Main.idr A tests/allschemes/channels006/expected R tests/{chez/channels005/run => allschemes/channels006/run} A tests/base/data_snoclist/SL.idr A tests/base/data_snoclist/expected A tests/base/data_snoclist/run A tests/base/data_string_parse_proof/StringParse.idr A tests/base/data_string_parse_proof/expected A tests/base/data_string_parse_proof/run A tests/base/deriving_foldable/DeriveFoldable.idr A tests/base/deriving_foldable/expected A tests/base/deriving_foldable/run A tests/base/deriving_functor/DeriveFunctor.idr A tests/base/deriving_functor/Search.idr A tests/base/deriving_functor/expected A tests/base/deriving_functor/run A tests/base/deriving_traversable/DeriveTraversable.idr A tests/base/deriving_traversable/expected A tests/base/deriving_traversable/run M tests/base/system_file_copyFile/run A tests/chez/chez035/Mod1.idr A tests/chez/chez035/Mod2.idr A tests/chez/chez035/expected A tests/chez/chez035/input A tests/chez/chez035/run A tests/chez/constfold/Check.idr A tests/chez/constfold/Fold.idr A tests/chez/constfold/expected A tests/chez/constfold/input A tests/chez/constfold/run A tests/chez/nat2fin/Check.idr A tests/chez/nat2fin/Test.idr A tests/chez/nat2fin/expected A tests/chez/nat2fin/input A tests/chez/nat2fin/run A tests/codegen/.gitignore D tests/codegen/builtin001/CatCases.idr M tests/codegen/builtin001/expected M tests/codegen/builtin001/run D tests/codegen/con001/CatCases.idr M tests/codegen/con001/run A tests/codegen/enum/Check.idr A tests/codegen/enum/Enum.idr A tests/codegen/enum/expected A tests/codegen/enum/input A tests/codegen/enum/run A tests/contrib/lexer/Test.idr A tests/contrib/lexer/expected A tests/contrib/lexer/run M tests/contrib/sortedmap_001/SortedMapTest.idr M tests/contrib/sortedmap_001/expected M tests/contrib/system_directory_tree_copyDir/run A tests/ideMode/ideMode005/Holes.idr M tests/ideMode/ideMode005/expected1 M tests/ideMode/ideMode005/expected9 M tests/ideMode/ideMode005/expectedC A tests/ideMode/ideMode005/expectedJ A tests/ideMode/ideMode005/inputJ M tests/ideMode/ideMode005/regenerate M tests/ideMode/ideMode005/run M tests/idris2/api001/LazyCodegen.idr M tests/idris2/basic044/expected M tests/idris2/basic049/Fld.idr M tests/idris2/basic049/expected M tests/idris2/debug001/expected M tests/idris2/docs004/expected M tests/idris2/evaluator002/expected A tests/idris2/evaluator004/Issue1282.idr A tests/idris2/evaluator004/expected A tests/idris2/evaluator004/input A tests/idris2/evaluator004/run M tests/idris2/interactive017/expected M tests/idris2/interactive030/expected M tests/idris2/interactive039/expected A tests/idris2/interactive043/ImplicitSplits.idr A tests/idris2/interactive043/expected A tests/idris2/interactive043/input A tests/idris2/interactive043/run A tests/idris2/interactive044/SplitShadow.idr A tests/idris2/interactive044/expected A tests/idris2/interactive044/input A tests/idris2/interactive044/run A tests/idris2/interactive045/Issue1742.idr A tests/idris2/interactive045/expected A tests/idris2/interactive045/input A tests/idris2/interactive045/run A tests/idris2/interface029/ForwardImpl1.idr A tests/idris2/interface029/ForwardImpl2.idr A tests/idris2/interface029/ForwardImpl3.idr A tests/idris2/interface029/expected A tests/idris2/interface029/run M tests/idris2/linear010/run M tests/idris2/linear011/run A tests/idris2/perror016/ParseIf.idr A tests/idris2/perror016/ParseIf2.idr A tests/idris2/perror016/ParseIf3.idr A tests/idris2/perror016/expected A tests/idris2/perror016/run A tests/idris2/perror017/ParseImpl.idr A tests/idris2/perror017/expected A tests/idris2/perror017/run A tests/idris2/perror018/ParseRecord.idr A tests/idris2/perror018/ParseRecord2.idr A tests/idris2/perror018/ParseRecord3.idr A tests/idris2/perror018/expected A tests/idris2/perror018/run A tests/idris2/perror019/ImplError.idr A tests/idris2/perror019/expected A tests/idris2/perror019/run M tests/idris2/pkg003/expected M tests/idris2/pkg006/depends/bar-baz/bar-baz.ipkg M tests/idris2/pkg006/depends/quux/quux.ipkg M tests/idris2/pkg006/expected M tests/idris2/pkg010/expected.in M tests/idris2/pkg010/run A tests/idris2/pkg013/.gitignore A tests/idris2/pkg013/depends/bar-0.7.2/bar.ipkg A tests/idris2/pkg013/depends/foo-0.1.0/foo.ipkg A tests/idris2/pkg013/expected.in A tests/idris2/pkg013/gen_expected.sh A tests/idris2/pkg013/run A tests/idris2/pkg013/test.ipkg A tests/idris2/pkg014/.gitignore A tests/idris2/pkg014/depends/bar-0.1.0/bar.ipkg A tests/idris2/pkg014/depends/bar-0.1.1/bar.ipkg A tests/idris2/pkg014/depends/baz-0.1.0/baz.ipkg A tests/idris2/pkg014/depends/baz-0.2.0/baz.ipkg A tests/idris2/pkg014/depends/baz-0.3.0/baz.ipkg A tests/idris2/pkg014/depends/foo-0.1.0/foo.ipkg A tests/idris2/pkg014/depends/foo-0.2.0/foo.ipkg A tests/idris2/pkg014/depends/foo-0.3.0/foo.ipkg A tests/idris2/pkg014/expected.in A tests/idris2/pkg014/gen_expected.sh A tests/idris2/pkg014/run A tests/idris2/pkg014/test.ipkg A tests/idris2/pkg015/depends/bar-0.1.0/bar.ipkg A tests/idris2/pkg015/depends/bar-0.1.1/bar.ipkg A tests/idris2/pkg015/depends/baz-0.1.0/baz.ipkg A tests/idris2/pkg015/depends/baz-0.2.0/baz.ipkg A tests/idris2/pkg015/depends/baz-0.3.0/baz.ipkg A tests/idris2/pkg015/depends/foo-0.1.0/foo.ipkg A tests/idris2/pkg015/depends/foo-0.2.0/foo.ipkg A tests/idris2/pkg015/depends/foo-0.3.0/foo.ipkg A tests/idris2/pkg015/depends/prz-0.1.0/prz.ipkg A tests/idris2/pkg015/expected A tests/idris2/pkg015/run A tests/idris2/pkg015/test.ipkg A tests/idris2/primloop/PrimLoop.idr A tests/idris2/primloop/expected A tests/idris2/primloop/input A tests/idris2/primloop/run A tests/idris2/record016/HoleRecord.idr A tests/idris2/record016/expected A tests/idris2/record016/input A tests/idris2/record016/run A tests/idris2/record017/RecordOptions.idr A tests/idris2/record017/expected A tests/idris2/record017/run M tests/idris2/reflection003/expected M tests/idris2/reflection004/refdecl.idr A tests/idris2/reflection015/MacroRetFunc.idr A tests/idris2/reflection015/expected A tests/idris2/reflection015/run A tests/idris2/reflection016/BindElabScBug.idr A tests/idris2/reflection016/Eta.idr A tests/idris2/reflection016/expected A tests/idris2/reflection016/input A tests/idris2/reflection016/run A tests/idris2/reflection017/CanElabType.idr A tests/idris2/reflection017/StillCantEscape.idr A tests/idris2/reflection017/expected A tests/idris2/reflection017/run A tests/idris2/rewrite001/Issue2573.idr A tests/idris2/rewrite001/expected A tests/idris2/rewrite001/run A tests/idris2/termination001/AgdaIssue6059.idr A tests/idris2/termination001/expected A tests/idris2/termination001/run A tests/idris2/unification001/Issue647.idr A tests/idris2/unification001/expected A tests/idris2/unification001/run M tests/idris2/warning003/expected M tests/idris2/with003/expected M tests/node/args/TestArgs.idr M tests/node/nomangle001/expected M tests/node/nomangle001/nomangle.idr M tests/node/nomangle002/expected M tests/node/nomangle002/nomangle1.idr M tests/node/nomangle002/nomangle2.idr M tests/node/tailrec001/expected M tests/node/tailrec001/tailrec.idr A tests/prelude/char001/chars.idr A tests/prelude/char001/expected A tests/prelude/char001/run D tests/racket/channels001/Main.idr D tests/racket/channels001/expected D tests/racket/channels001/run M tests/refc/buffer/run M tests/refc/garbageCollect/expected A www/README.md A www/katla.sh A www/source/index.md