Mathematics in VS Code with Lean

Formalizing mathematics is now possible in VS Code with Lean. See the manual here. Extension here.

Lean functionality is exposed in the UI via the universal quantifier at the top right of VS code.

Consider copying the MIL folder, containing key examples, so you can tinker with the example code.

MIL = Mathematics in Lean.

When you download the MIL, you will see a flurry of activity in your Output Console in VS Code. This will include reams of stuff relating to "Fetching Mathlib build artifact cache" and thousands of file downloads.

You will also see the incantation "lake build" which is the primary build command in the Lean build system.

Advice on how to work through the MIL textbook from the official website - "working through the exercises is central to the experience".

Note: when reading Lean files in VS code turn off Unicode character highlighting (Control-, to get into settings, and update Text Editor settings).

More on Data Validation in Pydantic

Pydantic Validation is the validation layer of the OpenAI SDK, the Google ADK, the Anthropic SDK, LangChain and others.

Pydantic uses Rust under the hood. This makes it faster than say, something implemented directly in Python.

How are the Python and Rust pieces glued together?

The key is that the validation layer is compiled in Rust (pydantic-core).  Data parsing, validation and in general, any perf-critical operations, are done here. Py03 is used to create bindings in Python.

While there is no need to use the Rust code directly, for reference it can be found in GitHub here.

But what does this validation actually entail?  What's the use case?

How does it work?

Type hints (PEP 484) are one of the tools used in Python validation (GvR himself h as co-authored that PEP).  Type hints enable integration with various static typing tools (like mypy) and IDEs (like VSCode).

The Type hints PEP also references PEP 3107 for function annotations (written by Collin Winter and Tony Lownds).

What is Pylance?

Pylance is the component that enables Visual Studio Code to provide IntelliSense for Python. 

It is underpinned by Microsoft's Pyright type checker (open source static type checker for Python). Read more about Pyright from the official website.

C/C++ on VS Code

You can edit C/C++ code in VS Code but you need the C/C++ Extension Pack for more features.

Microsoft's GitHub

Microsoft's GitHub is worth perusing from time-to-time. Some of the big projects are VS Code and TypeScript but many more additions are made to cover new directions like confidential computing.

Microsoft also have a website (opensource.microsoft.com) detailing their open source initiatives more broadly.  The Microsoft open source blog is also worth reading.

Replit versus GitHub Codespaces

Replit lets you build and run applications in the cloud, from within a web browser. GitHub Codespaces replicates VS Code in the cloud / kind of replicating a full dev setup in the cloud.

Compiling C# in VS Code

For this you need the C# Dev Kit extension. It's Roslyn-powered. 

The code name Roslyn was first written publicly by engineer Eric Lippert (the code was originally hosted on Microsoft's CodePlex before being moved to GitHub).

Dev Containers Extension in VS Code

What it is, What it does

The Dev Containers ("DC") extension is needed by Semantic Kernel in VS Code. It's worth expanding on its purpose here.

DC allows you to use a Docker container as a full-feature development environment (this is independent of how you deploy the thing).

More details here.

Dev Containers Dependencies

It requires Docker Desktop to be installed, which interacts with WSL2. If you don't have it, don't worry, however. VS Code will prompt you automatically to install it.  After installation, you will see a status bar labelled "Setting up Dev Containers" followed by "Connecting to Dev Container (show log)".

Dev Container Configuration

This is located in semantic-kernel\.devcontainer\devcontainer.json.  This is similar to launch.json for debugging configurations. More info here.

Allowing wsl.localhost in list of allowed hosts

When navigating to a directory in WSL from VS Code you may get the message:

The host 'wsl.localhost' was not found in the list of allowed hosts. Do you want to allow it anyway?

You will get the opportunity to hit Allow (because you trust the host, it is after all, your WSL installation) together with the option to flag: "Permanently allow host 'wsl.localhost'".

Microsoft Semantic Kernel

Microsoft Semantic Kernel is a "lighweight, open-source development kit" to build AI agents and integrate models into C#,  Python and Java code.

When you load up SK into a fresh Visual Studio Code (no extensions) it will prompt to install recommended extensions. These will include:

• ESLint - integrates ESLint JavaScript into VS Code (for static analysis)
  
• Prettier - integrates Prettier, the opinionated code formatter (for JavaScript, TypeScript and other webby stuff)
• Azure Functions - to quickly manage serverless apps directly from VS Code
• vscode-pdf - to display pdf files in VSCode (required to open PDF code maps for .NET and Python)

GitHub Desktop

GitHub Desktop enables you to work with projects hosted on GitHub. 

It is an open source application based on Electron (software framework to create desktop applications with web technologies: HTML, CSS and JavaScript with a Chromium browser engine front end and a Node.js backend, used in Visual Studio Code). 

Roughly speaking it is a visual version of the CLI. 

Building a VSCode Extension

It is important to know how to build a VSCode extension, not only in case you need one, but to know how one is built.  This guide will help you achieve this.  Note that it uses Yeoman, a "scaffolding tool for modern web apps", and a VSCode Extension Generator.

VSCode is Cool

Visual Studio Code is increasingly giving Microsoft Visual Studio a run for its money. 

One of the plus points of VSCode is it's lightweight as well as having built-in support for JavaScript, TypeScript and Node.js with other languages supported as extensions.