Skip to content

ReasLingo 基础操作 ​

ReasLingo 是搭载在整个 reaslab-agent 系统核心之上的原初智能体界面与架构。它负责统管所有工作区域的多轮自然语言对话,并且允许用户极致化调节 AI 的上下文结构与推理逻辑。

概述 ​

在任意项目中,无论您是编辑 Lean 证明还是优化数学模型,侧边栏均是由 ReasLingo UI 接手并提供 AI 驱动的核心服务驱动区域。

核心配置与用法 ​

@添加上下文 (Context Injection) ​

通过直接向提示词框输入带有 @ 的文件路径或直接右键文件选择 Add to Chat,您可使模型具有全局的代码库感知能力。同时在当前激活的文档中圈选部分高亮行,亦能极精细的只摘取当前代码切片发往大脑端进行特定重构工作。

配置高级引擎参数 ​

对话界面具有一系列深度开关和滑块调整项目底层模型的调用逻辑:

  • Max Tokens 输出限制: 根据您的诉求收紧或放大 AI 的回答篇幅容忍度。如果您意图让它生成代码或者分析多页文档,请将 max-tokens 设置至对应接口许可的高上限。
  • 配置推理强度 (Reasoning Effort): 选择偏向深思熟虑亦或者速答模式。当推理强度调高时,大模型后台架构能够对一些极高难度的 Lean 证明过程或是冗长的求解问题启用反思和复验逻辑。
  • 底层技能 (Skills) 引用: ReasLingo 支持读取规范化环境存储下的特定预写逻辑文件。只要向对应的系统路径添加技能机制,您的 AI 会立即继承并且在对话流内利用这份额外的工具或结构化回答思维提供服务。

在回复过程中排队和 Steer ​

AI 正在回复时输入框仍然可用,不必等这次回复结束。

  • Queue Message:把消息留到当前回复结束后再发出。按 Enter 或点击发送按钮。它适合安排接下来要做的事。
  • Steer:把消息立刻交给正在运行的任务。macOS 按 Cmd + Enter,Windows 和 Linux 按 Ctrl + Enter。它适合补充条件、纠正方向或缩小范围。

换行请按 Shift + Enter。以上操作在侧边栏对话和 Agent 模式中都可以用。

消息队列 ​

排队的消息显示在输入框正上方,最早的排在最前。每次回复结束后,队列中的下一条会自动发出。

调整顺序、Steer、编辑或撤回排队消息

  • 拖动每行左侧的手柄可以调整顺序。
  • 右侧三个图标依次是 Steer、Edit 和 Withdraw:把这条消息送进正在运行的任务、放回输入框,或从队列中删除。
  • Edit 也会把随消息一起添加的文件和代码片段放回输入区。
  • 带回形针图标的消息附有引用文件,悬停即可查看。

队列不为空时,Enter 会把消息追加到队列末尾,而不是开始新的回复。AI 正在回复且输入框为空时,发送按钮会变成 Stop Message,此时 Cmd/Ctrl + Enter 会 Steer 队列中的第一条消息。

回看之前的提问 ​

回看自己发过的消息有两组快捷键:方向键把提问调回输入框;Option/Alt + 方向键只在对话里滚动定位。

把提问调回输入框 ​

  • 按 ↑ 调出最近一次提问,继续按 ↑ 看更早的;按 ↓ 回到较新的。越过最新一条后,会恢复开始浏览前尚未发送的草稿。
  • 自己写的草稿有多行时,方向键先用于移动光标:到第一行再按 ↑、到最后一行再按 ↓,才会开始调取历史。调出的提问只要没改动,按 ↑ 就会继续往前翻。

在自己的消息之间跳转 ​

把焦点放在输入框或消息列表中,然后按住 macOS 的 Option (⌥) 或 Windows、Linux 的 Alt。

  • ↑ 滚动到上一条自己的消息,↓ 到下一条。
  • 需要时会自动加载更早的消息。越过最新一条后,视图回到对话底部。

对话操作 ​

每条消息下方有一排操作。最新一条回复上还会出现 Regenerate。

复制、分叉与重新生成

  • Copy message:把这一轮的文字复制到剪贴板。图标会短暂变成对勾。
  • Fork chat:从这条消息(含本条)截取对话,生成一个新会话并打开它。原来的会话保持不变。新会话标题会带上 (Fork)。当前回复还在生成时请等它结束再分叉。
  • Regenerate:只出现在最新一条消息上,且回复已经结束后才可点。它会把你的上一个问题再发送一次,并在后面追加新的回答。之前的回答仍留在对话里。

导出对话 ​

从历史记录导出对话

  1. 点击 ReasLingo 顶栏的 Chat History(时钟图标)。
  2. 把鼠标悬停在某个会话上。这一行会出现重命名、导出、发送副本和删除。
  3. 点击 Export chat(下载图标)。

下载的是 Markdown 文件:会话标题、导出时间、你的消息(引用格式)以及助手回复。