diff --git a/infoview/info.tsx b/infoview/info.tsx index 96d4e14..850616a 100644 --- a/infoview/info.tsx +++ b/infoview/info.tsx @@ -5,10 +5,11 @@ import { LocationContext, ConfigContext } from '.'; import { Widget } from './widget'; import { Goal } from './goal'; import { Messages, processMessages, ProcessedMessage, GetMessagesFor } from './messages'; -import { basename, useEvent } from './util'; -import { CopyToCommentIcon, PinnedIcon, PinIcon, ContinueIcon, PauseIcon, RefreshIcon, GoToFileIcon } from './svg_icons'; +import { basename, useEvent, delayedThrottled } from './util'; +import { CopyToCommentIcon, PinnedIcon, PinIcon, ContinueIcon, PauseIcon, RefreshIcon, GoToFileIcon, DoSuggestIcon, DoNotSuggestIcon } from './svg_icons'; import { Details } from './collapsing'; import { Event, InfoResponse, CurrentTasksResponse, Message } from 'lean-client-js-core'; +import { Suggestor } from './suggestions'; /** Older versions of Lean can't deal with multiple simul info requests so this just prevents that. */ class OneAtATimeDispatcher { @@ -63,24 +64,6 @@ function useMappedEvent(ev: Event, initial: S, f: (_: T) => S, deps?: R return s; } -// returns function that triggers `cb` -// - but only ms milliseconds after the first call -// - and not more often than once every ms milliseconds -function delayedThrottled(ms: number, cb: () => void): () => void { - const waiting = React.useRef(false); - const callbackRef = React.useRef<() => void>(); - callbackRef.current = cb; - return () => { - if (!waiting.current) { - waiting.current = true; - setTimeout(() => { - waiting.current = false; - callbackRef.current(); - }, ms); - } - }; -} - interface InfoState { loc: Location; loading: boolean; @@ -144,6 +127,7 @@ export function Info(props: InfoProps): JSX.Element { const {isCursor, isPinned, onPin} = props; const [isPaused, setPaused] = React.useState(false); + const [doSuggest, setDoSuggest] = React.useState(false); const isCurrentlyPaused = React.useRef(); isCurrentlyPaused.current = isPaused; @@ -194,6 +178,7 @@ export function Info(props: InfoProps): JSX.Element { { e.preventDefault(); onPin(!isPinned)}} title={isPinned ? 'unpin' : 'pin'}>{isPinned ? : } { e.preventDefault(); setPaused(!isPaused)}} title={isPaused ? 'continue updating' : 'pause updating'}>{isPaused ? : } { !isPaused && { e.preventDefault(); forceUpdate(); }} title="update"> } + { e.preventDefault(); setDoSuggest(!doSuggest)}} title={doSuggest ? 'stop ML suggestions' : 'activate ML suggestions'}>{doSuggest ? : }
@@ -225,6 +210,9 @@ export function Info(props: InfoProps): JSX.Element {
+ {(doSuggest && goalState) ?
+ +
: null } {nothingToShow && ( loading ? 'Loading...' : isPaused ? Updating is paused. forceUpdate()}>Refresh or setPaused(false)}>resume updating to see information : diff --git a/infoview/server.ts b/infoview/server.ts index f8e5d85..929e63d 100644 --- a/infoview/server.ts +++ b/infoview/server.ts @@ -1,5 +1,8 @@ import { Server, Transport, Connection, Event, TransportError, Message } from 'lean-client-js-core'; -import { ToInfoviewMessage, FromInfoviewMessage, Config, Location, defaultConfig, PinnedLocation, InsertTextMessage } from '../src/shared'; +import { + ToInfoviewMessage, FromInfoviewMessage, Config, Location, defaultConfig, PinnedLocation, InsertTextMessage, + SuggestionsErrorInt, SuggestionsInt +} from '../src/shared'; declare const acquireVsCodeApi; // eslint-disable-next-line @typescript-eslint/no-unsafe-assignment const vscode = acquireVsCodeApi(); @@ -45,6 +48,8 @@ export const TogglePinEvent: Event = new Event(); export const ServerRestartEvent: Event = new Event(); export const AllMessagesEvent: Event = new Event(); export const ToggleAllMessagesEvent: Event = new Event(); +export const SuggestionsErrorEvent: Event = new Event(); +export const SuggestionsEvent: Event = new Event(); export let currentAllMessages: Message[] = []; AllMessagesEvent.on((msgs) => currentAllMessages = msgs); @@ -69,6 +74,8 @@ window.addEventListener('message', event => { // messages from the extension case 'toggle_all_messages': ToggleAllMessagesEvent.fire({}); break; case 'server_event': break; case 'server_error': break; + case 'Suggestions_error': SuggestionsErrorEvent.fire(message); break; + case 'Suggestions': SuggestionsEvent.fire(message); break; } }); diff --git a/infoview/suggestions.tsx b/infoview/suggestions.tsx new file mode 100644 index 0000000..5344c88 --- /dev/null +++ b/infoview/suggestions.tsx @@ -0,0 +1,149 @@ +import * as React from 'react'; +import { WidgetIdentifier } from 'lean-client-js-core'; +import { SuggestionsInfoStatus, SuggestionsInt, SuggestionsModelResult, SuggestionsTacticInfo } from '../src/shared'; +import { useEvent, delayedThrottled } from './util'; +import { SuggestionsEvent, SuggestionsErrorEvent, post } from './server'; + +const statusColTable: { [T in SuggestionsInfoStatus]: string } = { + 'loading': 'gold', + 'error': 'dark-red', + 'valid': 'green', + 'solving': 'blue', + 'done': '' +} +interface SuggestionsProps { + widget: WidgetIdentifier; + goalState: string; +} + +function SingleTacticInfo(props: { tacticInfo: SuggestionsTacticInfo, widget: WidgetIdentifier}): JSX.Element { + return ( + { + e.preventDefault(); + post({ + command: 'insert_text', + text: `${props.tacticInfo.tactic},`, + insert_type: 'relative' + }) + }} + > + {props.tacticInfo.tactic} + + ) +} + + +function Waiter(): JSX.Element { + const [count, setCount] = React.useState(0); + React.useEffect(() => { + const interval = setInterval(() => setCount((count + 1) % 4), 500); + return () => clearInterval(interval); + }, [count]); + return {'.'.repeat(count)}; +} + +function Suggestions(props: { + goalState: string, reqId: number, widget: WidgetIdentifier +}) { + const [status, setStatus] = React.useState('loading'); + const [errorMsg, setErrorMsg] = React.useState(); + const [suggestionsResults, setSuggestionsResults] = React.useState(); + + // get Suggestions results - set Suggestions results + useEvent( + SuggestionsEvent, + (suggestions: SuggestionsInt) => { + if (suggestions.results && props.reqId === suggestions.reqId) { + if (suggestions.results.error) { + setErrorMsg(suggestions.results.error); + setStatus('error'); + } else { + setSuggestionsResults(suggestions.results); + setStatus('done'); + } + } + }, + [props.reqId] + ); + + React.useEffect(() => { + setStatus('loading'); + setErrorMsg(undefined); // reset error msg + }, [props.reqId]); + + return props.goalState && ( +
+
+ {['loading', 'error'].includes(status) ? +

+ {status === 'loading' ? 'Querying Suggestions' : 'Something went wrong :('} + {status === 'loading'? : null} +

+ : null} + {errorMsg ? {errorMsg} : null} + {(['done', 'checking'].includes(status) && suggestionsResults && !suggestionsResults.error && suggestionsResults.tactic_infos) ? +
{Object.values(suggestionsResults.tactic_infos).map( + tactic_info =>

+ )}
+ : null + } +
+
+ ); +} + +export function Suggestor(props: SuggestionsProps): JSX.Element { + const [suggReqId, setSuggReqId] = React.useState(0); + const [doSuggest, setDoSuggest] = React.useState(false); + const [errorMsg, setErrorMsg] = React.useState(); + const [prefix, setPrefix] = React.useState(''); + + useEvent( + SuggestionsErrorEvent, + (s) => { + setErrorMsg(s.error); + }, [] + ); + + React.useEffect(() => { + setDoSuggest(true); + }, [prefix, props.goalState]) + React.useEffect(delayedThrottled( + 300, + () => { + if (doSuggest) setDoSuggest(false); + else return; + if (props.goalState !== undefined && props.goalState !== 'no goals') { + setSuggReqId(rid => { + post({ + command: 'get_suggestions', + reqId: rid + 1, + goalState: props.goalState, + prefix + }); + setErrorMsg(undefined); // reset error msg + return rid + 1 + }); + } + } + ), [prefix, props.goalState, doSuggest]) + + const inputProps = { style: { display: 'inline' }, type: 'text', size: 12, value: prefix }; + + return ( +
+ {errorMsg + ? {errorMsg} + :
+
e.preventDefault()}> + Tactic suggestions with prefix: + setPrefix(e.target.value)} /> +
+ +
+ } +
+ ); +} \ No newline at end of file diff --git a/infoview/svg_icons.tsx b/infoview/svg_icons.tsx index 934a9ea..d1c049a 100644 --- a/infoview/svg_icons.tsx +++ b/infoview/svg_icons.tsx @@ -46,4 +46,20 @@ export function GoToFileIcon(): JSX.Element { export function ClippyIcon(): JSX.Element { return ; -} \ No newline at end of file +} + +export function DoSuggestIcon(): JSX.Element { + return + + + +} + +export function DoNotSuggestIcon(): JSX.Element { + return + + + + +} + diff --git a/infoview/util.tsx b/infoview/util.tsx index 5c3d181..82d93c8 100644 --- a/infoview/util.tsx +++ b/infoview/util.tsx @@ -1,6 +1,21 @@ import * as React from 'react'; import { Event } from 'lean-client-js-core'; +export function delayedThrottled(ms: number, cb: () => void): () => void { + const waiting = React.useRef(false); + const callbackRef = React.useRef<() => void>(); + callbackRef.current = cb; + return () => { + if (!waiting.current) { + waiting.current = true; + setTimeout(() => { + waiting.current = false; + callbackRef.current(); + }, ms); + } + }; +} + /** Split a string by a regex, executing `f_no_match` on the pieces which don't match, `f_match` on the pieces which do, and concatenating the results into an array. */ export function regexMap(regex: RegExp, s: string, f_no_match: (snm : string) => T, f_match: (m : RegExpExecArray) => T ) : T[] { diff --git a/package.json b/package.json index f72caef..b22b6c0 100644 --- a/package.json +++ b/package.json @@ -24,6 +24,16 @@ "default": "lean", "markdownDescription": "Path to the Lean executable to use. **DO NOT CHANGE** from the default `lean` unless you know what you're doing!" }, + "lean.suggestionURL": { + "type": "string", + "default": "", + "markdownDescription": "URL to contact for model suggestions" + }, + "lean.suggestionAPIKey": { + "type": "string", + "default": "", + "markdownDescription": "API Key to use for suggestions" + }, "lean.leanpkgPath": { "type": "string", "default": "leanpkg", diff --git a/src/infoview.ts b/src/infoview.ts index f1d4d85..853edc3 100644 --- a/src/infoview.ts +++ b/src/infoview.ts @@ -1,5 +1,8 @@ import { InfoResponse, Connection } from 'lean-client-js-node'; +import { WidgetIdentifier, Request, GetWidgetRequest } from 'lean-client-js-core'; import { join } from 'path'; +import { AxiosRequestConfig, AxiosResponse } from 'axios'; +import axios from 'axios'; import { commands, Disposable, DocumentSelector, ExtensionContext, languages, Position, Range, @@ -8,7 +11,10 @@ import { Uri, ViewColumn, WebviewPanel, window, workspace, env, } from 'vscode'; import { Server } from './server'; -import { ToInfoviewMessage, FromInfoviewMessage, PinnedLocation, InsertTextMessage, ServerRequestMessage, RevealMessage, HoverPositionMessage, locationEq, Location, InfoViewTacticStateFilter } from './shared' +import { + ToInfoviewMessage, FromInfoviewMessage, PinnedLocation, InsertTextMessage, ServerRequestMessage, RevealMessage, HoverPositionMessage, locationEq, Location, InfoViewTacticStateFilter, + SuggestionsModelResult +} from './shared' import { StaticServer } from './staticserver'; import { CodePointPosition } from './utils/utf16Position'; @@ -214,6 +220,9 @@ export class InfoProvider implements Disposable { await this.sendConfig(); await this.postMessage({command: 'all_messages', messages: this.server.messages}); return; + case 'get_suggestions': + this.getSuggestions(message.reqId, message.goalState, message.prefix); + return; } } private handleServerRequest(message: ServerRequestMessage) { @@ -345,7 +354,7 @@ export class InfoProvider implements Disposable { private getActiveCursorLocation(): Location | null { if (!window.activeTextEditor || !languages.match(this.leanDocs, window.activeTextEditor.document)) {return null; } - let p = CodePointPosition.ofPosition(window.activeTextEditor.document, window.activeTextEditor.selection.active); + const p = CodePointPosition.ofPosition(window.activeTextEditor.document, window.activeTextEditor.selection.active); return this.makeLocation(window.activeTextEditor.document.fileName, p); } @@ -388,4 +397,45 @@ export class InfoProvider implements Disposable { ` } + + private getSuggestions(reqId: number, goalState: string, prefix: string): void { + const api_key : string = workspace.getConfiguration('lean').get('suggestionAPIKey'); + const url : string = workspace.getConfiguration('lean').get('suggestionURL'); + if (!url) { + void this.postMessage({ + command: 'Suggestions', + results: {'error': 'lean.suggestionURL not set, please ask on Zulip for URL and API key.'}, + reqId, + }); + return + } + if (goalState === 'no goals') { return; } + const data = JSON.stringify({ + tactic_state: goalState, + prefix + }); + const config: AxiosRequestConfig = { + headers: { + 'Content-Type': 'application/json;charset=utf-8', + 'Content-Length': Buffer.byteLength(data), + 'x-api-key': api_key, + } + }; + axios.post(url, data, config).then( + (response: AxiosResponse) => { + void this.postMessage({ + command: 'Suggestions', + results: response.data, + reqId + }); + }, + (reason) => { + void this.postMessage({ + command: 'Suggestions_error', + error: `failed to post ${data} for the following reason: ${reason}` + }); + } + ); + } + } diff --git a/src/shared.ts b/src/shared.ts index abd90de..b240e9c 100644 --- a/src/shared.ts +++ b/src/shared.ts @@ -1,6 +1,7 @@ /* This file contains all of the types that are common to the extension and the infoview. */ import { Message, Task } from 'lean-client-js-node'; +import { WidgetIdentifier } from 'lean-client-js-core'; // import { ServerStatus } from './server'; @@ -101,13 +102,50 @@ export type FromInfoviewMessage = | SyncPinMessage | {command: 'request_config'} | {command: 'copy_text'; text: string} + | {command: 'get_suggestions'; reqId: number; goalState: string, prefix: string} /** Message from the extension to the infoview. */ export type ToInfoviewMessage = - | { command: 'server_event' | 'server_error'; payload: string} // payloads have to be stringified json because vscode crashes if the depth is too big. } - | { command: 'position'; loc: Location} - | { command: 'on_config_change'; config: Partial} - | { command: 'all_messages'; messages: Message[]} + | { command: 'server_event' | 'server_error'; payload: string } // payloads have to be stringified json because vscode crashes if the depth is too big. } + | { command: 'position'; loc: Location } + | { command: 'on_config_change'; config: Partial } + | { command: 'all_messages'; messages: Message[] } | { command: 'toggle_all_messages' } | SyncPinMessage - | { command: 'pause' | 'continue' | 'toggle_updating' | 'copy_to_comment' | 'toggle_pin' | 'restart'} \ No newline at end of file + | { command: 'pause' | 'continue' | 'toggle_updating' | 'copy_to_comment' | 'toggle_pin' | 'restart'} + | SuggestionsErrorInt + | SuggestionsInt + + +export interface SuggestionsError { + error: string; +} + +export interface SuggestionsErrorInt extends SuggestionsError { + command: 'Suggestions_error'; +} + +export type SuggestionsInfoStatus = 'loading' | 'error' | 'done' | 'valid' | 'solving'; + +export interface SuggestionsReqId { + reqId: number; +} + +export interface SuggestionsTacticInfo { + tactic: string; + next_ts?: string; + n_subgoals?: number; + error?: string; + status?: SuggestionsInfoStatus; // actually 'loading' is not possible + message?: string; +} + +export interface SuggestionsModelResult { + tactic_infos?: SuggestionsTacticInfo[]; + error?: string; +} + +export interface SuggestionsInt extends SuggestionsReqId { + command: 'Suggestions'; + results: SuggestionsModelResult; +}